]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2012-01-08 Ferruccio Guidi- notation restyling ...
2012-01-07 Ferruccio GuidiBasic_2: - we addedsome files
2012-01-07 Ferruccio Guidilambda_delta: global environments handling: redefined...
2012-01-04 Ferruccio Guidithe support for reducibility candidates evolves ,,,,
2012-01-03 Andrea AspertiComplete version
2012-01-03 Andrea Aspertimodified definition of memb
2012-01-03 Andrea Aspertireverse
2012-01-03 Andrea Aspertimore properties of union
2012-01-03 Andrea Aspertinoteq_to_eqnot
2011-12-26 Ferruccio Guidinotation and dependences bug fix
2011-12-25 Ferruccio GuidiBasic 2 page update
2011-12-25 Ferruccio Guidi- support for candidates of reducibility continues ...
2011-12-20 Ferruccio GuidiBasic_2 update ...
2011-12-20 Ferruccio Guidi- the definition of the framework for strong normalizat...
2011-12-16 Andrea AspertiIn case paramodulation fails we apply unit equalities.
2011-12-15 Andrea AspertiSplitted DeqSets in their own file. Notation for memb...
2011-12-15 Andrea AspertiHints sui DeqSets
2011-12-14 Claudio Sacerdoti... More stuff from CerCo to the standard library.
2011-12-14 Claudio Sacerdoti... Some more lemmas from CerCo.
2011-12-14 Wilmer RicciottiMatitaweb: large commit porting to the new Matita 0...
2011-12-14 Claudio Sacerdoti... 1) Notation for dependent pairs differentiated from...
2011-12-13 Claudio Sacerdoti... Dependent pairs (i.e. Sigma types in Type[0]) are back...
2011-12-13 Claudio Sacerdoti... 1) PSig and Sig merged into a single Sigma type in...
2011-12-13 Claudio Sacerdoti... inject/eject replaced by mk_Sig/pi1.
2011-12-13 Claudio Sacerdoti... 1) New file russell with the coercions to activate...
2011-12-13 matitawebChapter 5 = re.ma ; chapter 6 = moves.ma
2011-12-13 matitawebNew chapter 4
2011-12-13 Wilmer RicciottiMatitaweb: clicking buttons disables the GUI to prevent...
2011-12-13 Andrea AspertiSplitted re into lang.ma nd re.ma
2011-12-13 Andrea AspertiSig in Prop
2011-12-13 Claudio Sacerdoti... More stuff integrated from CerCo on sigma types (that...
2011-12-13 Enrico Tassiaxiom-
2011-12-12 Claudio Sacerdoti... pair => mk_Prod (one more was left in notation)
2011-12-12 Claudio Sacerdoti... precedence level of if-then-else fixed
2011-12-12 Claudio Sacerdoti... Added elimination principles for destructuring let...
2011-12-12 Claudio Sacerdoti... Some integrations from CerCo. In particular:
2011-12-12 Enrico Tassisupport -axiom to avoind indexing an axiom (since there...
2011-12-12 Ferruccio Guidi- we improved and updated the generated web pages
2011-12-12 Claudio Sacerdoti... Pairs are now records.
2011-12-12 Claudio Sacerdoti... Parentheses are now needed. I do not know why and when...
2011-12-12 Wilmer RicciottiMatitaweb: changes to matitadaemon.ml to make it work...
2011-12-12 Wilmer RicciottiMatitaweb: added utility for conversion of user dbs...
2011-12-12 Claudio Sacerdoti... Re-Ported to
2011-12-12 Wilmer RicciottiMatitaweb: secure SHA-256 encryption for passwords.
2011-12-12 matitawebcommit by user andrea
2011-12-12 matitawebcommit by user andrea
2011-12-12 matitawebcommit by user andrea
2011-12-12 matitawebcommit by user andrea
2011-12-12 Ferruccio Guidinat library reorganized ....
2011-12-12 Andrea AspertiGeneralization to any alphabet. We do not need a finite
2011-12-11 Ferruccio Guidi- slicing relation for the global environment defined...
2011-12-09 Andrea Aspertilist.ma moved inside lists.
2011-12-09 Andrea Asperticlosing more axioms
2011-12-08 Ferruccio Guidiupdating the information on lambda_delta
2011-12-08 Ferruccio GuidiMaietty suggested to change a paragraph on the devel...
2011-12-08 Ferruccio GuidiMaietti suggested to replace a paragraph about the...
2011-12-07 Andrea AspertiClosing some axioms...
2011-12-07 Andrea Asperti\vee notation for boolean or
2011-12-06 Ferruccio Guidinew files started ...
2011-12-06 Ferruccio Guidiother addition to the standard library removed
2011-12-06 Ferruccio Guidiwe added a definition and a couple of lemmas
2011-12-06 Ferruccio Guidi- support for atomic arities and candidates of reducibi...
2011-12-06 Wilmer RicciottiGrammar change: let corecs can take no arguments (and...
2011-12-06 Wilmer RicciottiFixes a bug that overwrited the index of the recursive...
2011-12-06 Andrea AspertiListb contains some boolean functions over lists.
2011-12-06 Wilmer RicciottiMatitaweb:
2011-12-06 Andrea Aspertinaive sets (A-> Prop)
2011-12-05 Andrea AspertiMore properties of iff
2011-12-05 Andrea AspertiDecidability of equality (draft)
2011-11-26 Ferruccio Guidicomponent "reducibility" updated to new syntax!
2011-11-26 Ferruccio Guidicomponent "unfold" updated to new syntax ...
2011-11-26 Ferruccio Guidicomponent "substitution" updated to new syntax ...
2011-11-26 Ferruccio Guidi- "grammar" component updated to new syntax ...
2011-11-25 Ferruccio GuidiGround_2 ported to new syntax ...
2011-11-25 Ferruccio Guidibugfix in clearing the replaced variable: a relocation...
2011-11-24 Ferruccio GuidiDestruct: we warn about the substituted variable to...
2011-11-24 Ferruccio Guidi- now destruct tries to clear the replaced variables...
2011-11-24 Enrico Tassifixed DESTDIR
2011-11-24 Enrico Tassifixed DESTDIR
2011-11-22 Claudio Sacerdoti... Changes to disambiguation:
2011-11-21 Ferruccio GuidiBasic_2 file names update
2011-11-21 Claudio Sacerdoti... Syntax change: change where what => change what where.
2011-11-21 Andrea Aspertiregular expressions
2011-11-21 Andrea AspertiFiltering all equations that cannot be embedded (contai...
2011-11-21 Andrea AspertiPassing the correct subst a metasenv when idexing local...
2011-11-21 Andrea AspertiPassing the right subst and metasenv when indexing...
2011-11-21 Andrea AspertiAdded a test for paramodulation filtering terms with...
2011-11-21 Andrea AspertiMore debugging info
2011-11-21 Andrea AspertiAssert false removed (in line with the variable case).
2011-11-21 Claudio Sacerdoti... {pattern} => in pattern;
2011-11-21 Claudio Sacerdoti... {pattern} => in pattern;
2011-11-21 Andrea AspertiTypo in comment
2011-11-18 Enrico Tassihints
2011-11-18 Enrico Tassicoercions
2011-11-18 Wilmer RicciottiSolves a bug that caused the auto statistics to refer...
2011-11-18 Wilmer RicciottiAdded help for discriminator and inverter.
2011-11-18 Enrico Tassishort notation for "coercion"
2011-11-18 Claudio Sacerdoti... ...
2011-11-18 Claudio Sacerdoti... ...
2011-11-18 Enrico Tassiminor Makefile fixes for the release
next