]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2010-04-19 Andrea Aspertialpha_eq instead of pervasives.compare
2010-04-15 Enrico Tassibool_ext on 'o' not on 'Prop' (they are convertible...
2010-04-14 Claudio Sacerdoti... ...
2010-04-14 Claudio Sacerdoti... ...
2010-04-14 Claudio Sacerdoti... Formal points.
2010-04-14 Claudio Sacerdoti... Some dualization clean-up.
2010-04-13 Enrico Tassifixed makefile
2010-04-13 Enrico Tassiauto destructs while introducing in the context
2010-04-13 Enrico Tassiprint nobjects (hack with Obj.magic)
2010-04-13 Enrico Tassicatch the right exception, avoid uncaught Subst_not_found
2010-04-13 Enrico Tassisame heads different arity -> INCOMPARABLE
2010-04-13 Enrico Tassisome fixes to THF parser
2010-04-13 Enrico Tassifixed support file for TPTP
2010-04-11 Ferruccio Guidithe edges must be quoted as well (not only the nodes)
2010-04-09 Andrea Aspertiapply_subst_context on statuses
2010-04-08 Enrico Tassi...
2010-04-08 Enrico Tassisupport axioms
2010-04-08 Enrico Tassi...
2010-04-08 Enrico Tassithf problems list for tptp 4.0.1
2010-04-08 Enrico Tassifixed compiltion order of lexer/parser
2010-04-08 Claudio Sacerdoti... New code (unbranched) to compute all keys by all possib...
2010-04-08 Claudio Sacerdoti... New sets of.
2010-04-08 Enrico TassiTHF parser received some care
2010-04-08 Andrea AspertiFixing indexing (commit parziale di Claudio?)
2010-04-07 Enrico TassiTHF parser for TPTP
2010-03-31 Claudio Sacerdoti... Not is now inductive.
2010-03-31 Claudio Sacerdoti... Use the inversion!
2010-03-31 Claudio Sacerdoti... Bug fixed: the current equation is not always the last...
2010-03-31 Claudio Sacerdoti... ...
2010-03-31 Claudio Sacerdoti... - inversion principles are now generated also for co...
2010-03-31 Claudio Sacerdoti... More debugging info from print_tac.
2010-03-31 Claudio Sacerdoti... Implicit and UserInput were printed incorrectly.
2010-03-31 Claudio Sacerdoti... ninversion
2010-03-31 Andrea Aspertiremoved boh
2010-03-31 Wilmer RicciottiAdded test file for inversion in ng matita.
2010-03-31 Andrea AspertiTracing mechanism for auto. Interface changed to solve...
2010-03-26 Claudio Sacerdoti... Good definition found.
2010-03-26 Claudio Sacerdoti... (Co)Inductively Generated Formal Topologies (not only...
2010-03-25 Matthias Puechpatched the definition of locate, advances in locate_ad...
2010-03-25 Wilmer RicciottiZ.ma updated to reflect changes in the logical Not...
2010-03-25 Matthias PuechAutomation problem
2010-03-25 Andrea AspertiMore work
2010-03-25 Andrea Asperticosi va (se vi pare).
2010-03-25 Claudio Sacerdoti... ...
2010-03-25 Andrea AspertiConflict(?).
2010-03-25 Andrea AspertiExtension of demod to arbtrary predicates (not just...
2010-03-24 Claudio Sacerdoti... Nice examples for automation (that fails).
2010-03-24 Claudio Sacerdoti... Simplified proof after pattern fix
2010-03-24 Claudio Sacerdoti... "Not" is no longer a definition
2010-03-24 Claudio Sacerdoti... The precedence of ^-1 has changed.
2010-03-24 Claudio Sacerdoti... Equality has one right parameter and thus it's eliminat...
2010-03-24 Claudio Sacerdoti... ...
2010-03-24 Claudio Sacerdoti... Axioms were not indexed.
2010-03-24 Claudio Sacerdoti... Axioms were not indexed.
2010-03-24 Claudio Sacerdoti... ...
2010-03-24 Claudio Sacerdoti... Real numbers as co-inductive streams of digits (overlap...
2010-03-24 Andrea AspertiComputation of the trace.
2010-03-23 Matthias Puechtypo in a proof
2010-03-23 Andrea AspertiOne more case.
2010-03-23 Andrea AspertiReadded eqf_2.
2010-03-23 Andrea Aspertisymmetric_eq -> sym_eq
2010-03-23 Andrea AspertiRe-proved an axiom
2010-03-23 Andrea AspertiCommented a few lemmas (copies).
2010-03-23 Andrea AspertiFixed a few bugs
2010-03-23 Andrea Asperti"flat" function (subst unfolding)
2010-03-23 Andrea AspertiKeeping only lift_aux e subst_aux (renamed to lift...
2010-03-23 Andrea AspertiMoved compare in a different file.
2010-03-18 Matthias PuechDowngrading level of infix notations involving \sup.
2010-03-18 Andrea AspertiPorting alla nuova def. di negazione
2010-03-18 Andrea AspertiNuova versione di not.
2010-03-18 Andrea AspertiPrintings removed.
2010-03-18 Andrea AspertiDebugging disabled.
2010-03-18 Andrea AspertiDebugging disabled.
2010-03-18 Andrea AspertiNew demodulation tactics (mostly for debugging purposes).
2010-03-18 Andrea AspertiExporting the demodulation function.
2010-03-18 Andrea AspertiNew option "demod" for auto.
2010-03-18 Andrea AspertiPorting the new definition of equality.
2010-03-18 Claudio Sacerdoti... Do not index examples (concrete syntax: nremark).
2010-03-18 Claudio Sacerdoti... nremark => `Example (not to be indexed)
2010-03-18 Andrea Aspertiapp of app inside smart application.
2010-03-17 Ferruccio Guididr
2010-03-17 Andrea Aspertiqualche caso del lemma 5.2.11
2010-03-17 Claudio Sacerdoti... OCaml's inferred type simplified.
2010-03-17 Claudio Sacerdoti... ...
2010-03-17 Andrea AspertiSplitted gpts in two files.
2010-03-17 Andrea AspertiAggiornamento alla negazione.
2010-03-17 Andrea AspertiNuova definizione della negazione.
2010-03-16 Claudio Sacerdoti... Comparison of two applications with a different number...
2010-03-16 Claudio Sacerdoti... 1) intros cleans up the cache (because the context...
2010-03-16 Claudio Sacerdoti... refreshing of inferred type was missing
2010-03-16 Claudio Sacerdoti... ...
2010-03-12 Andrea AspertiFirst version of PTS
2010-03-12 Andrea AspertiNew definition of negation
2010-03-12 Andrea AspertiSubst was missing in perforate small (apparently, gty...
2010-03-12 Andrea Aspertiremoved debug from the inteface
2010-03-04 Andrea AspertiIn line with the ml.
2010-03-04 Andrea Asperti1. For smart application, we only perforate small terms...
2010-03-04 Andrea AspertiSmall changes for debugging
2010-03-04 Andrea AspertiFixed a bug in deep_eq: we generated new clauses but...
2010-03-04 Andrea AspertiCorrected a bug relative to the application of substs...
next