]> matita.cs.unibo.it Git - helm.git/history - matita/matita/lib
some notation renamed and fixed
[helm.git] / matita / matita / lib /
2014-01-28 Andrea AspertiAlmost there
2014-01-28 Andrea Aspertiprogress
2014-01-27 Andrea Aspertiworking version
2014-01-26 Ferruccio Guidinat: we added a non-indexed theorem
2014-01-26 Andrea Aspertimore auxiliary machines
2014-01-26 Ferruccio Guidi- nat: some additions, plus_minus_commutative renamed...
2013-12-04 Andrea AspertiNew approach: we use "iterator" steps in place of pointers.
2013-12-02 Claudio Sacerdoti... 1. more bugs fixed
2013-12-02 Claudio Sacerdoti... More progress.
2013-12-02 Claudio Sacerdoti... Some progress in the correctness proof and a bug fixed.
2013-11-29 Andrea AspertiA first example that uses a status monad where the...
2013-11-26 Ferruccio Guidi- natural numbers with infinity for lambdadelta
2013-11-25 Ferruccio Guidi- xoa: the definitions file now includes the notations...
2013-11-15 Wilmer RicciottiFinal version of the binary machine (all proofs completed).
2013-11-07 Wilmer RicciottiCloses many daemons.
2013-11-06 Wilmer RicciottiFull rework of the semantics of the binary machine...
2013-11-03 Wilmer RicciottiAlmost finished...
2013-11-03 Wilmer RicciottiMajor bugfix/reorganization/improvement of the partial...
2013-10-28 Andrea AspertiSplitted star
2013-10-25 Andrea Aspertifull.ma
2013-10-24 Andrea Aspertistep (almost) done
2013-10-24 Andrea AspertiThe step machine (draft)
2013-10-24 Andrea Aspertimany changes
2013-10-20 Wilmer RicciottiCompletes all the phases of the binary machine (modulo...
2013-10-19 Andrea AspertiSlowly porting to an enriched tape alphabet
2013-10-18 Andrea AspertiThe moves (almost)
2013-10-15 Andrea Aspertiadded sem_seq_app for the mono case
2013-10-15 Andrea Aspertirenaming files
2013-10-14 Andrea Aspertialmost there
2013-10-14 Wilmer RicciottiCompleted phases 0, 1, and 3.
2013-10-12 Andrea AspertiStill a problem to be fixed: after reaching the border...
2013-10-12 Andrea Aspertishift a trace from an extremity
2013-10-12 Andrea Aspertisplitting files
2013-10-12 Andrea AspertiMoved multi_to_mono.ma inside multi_to_mono
2013-10-09 Wilmer Ricciottiprogress in the semantics of binary machines
2013-10-07 Wilmer RicciottiStarting proof about semantics of binary machines.
2013-10-07 Wilmer RicciottiCompletes the definition of binaryTM.
2013-10-06 Andrea Aspertiprogress in the deifinition of the semantics of the...
2013-10-03 Wilmer RicciottiAdds transformation of generic monotape machines into...
2013-10-02 Andrea Aspertia vector of finsets is a finset (in progress)
2013-09-07 Ferruccio Guidisupport for nat-labeled reflexive and transitive closur...
2013-08-09 Ferruccio Guidi- we added nat-labeled reflexive and transitive closure...
2013-08-01 Ferruccio Guidipartial commit: just the components before "static...
2013-06-19 Ferruccio Guidi- partial commit :(
2013-06-05 Ferruccio Guidisome work on extended reduction ...
2013-05-31 Andrea Aspertiiteration.ma
2013-05-31 Andrea Aspertibounded quantifiers and pidgeon_hole
2013-05-31 Andrea Aspertigap.ma
2013-05-17 Andrea AspertiImproved version
2013-05-17 Andrea Aspertimore functions
2013-05-03 Andrea Aspertireverse complexity
2013-04-30 Claudio Sacerdoti... Missing include.
2013-04-30 Andrea Aspertichapter9
2013-04-30 Andrea Aspertitutorial
2013-04-30 Claudio Sacerdoti... Old version dropped.
2013-04-30 Andrea AspertiNew notation for congruence
2013-04-30 Andrea AspertiThis line, and those below, will be ignored--
2013-04-29 Andrea AspertiA few integrations (closed an axiom in finset).
2013-04-25 Wilmer RicciottiAn attempt at ostensiby named syntax.
2013-03-11 Andrea AspertiChpater 4 and 5
2013-03-10 Andrea Aspertichapters 2 e 3
2013-02-28 Ferruccio Guidi- lambdadelta: first recursive part of preservation...
2013-02-28 Andrea Aspertichapter2 revisited
2013-02-27 Andrea AspertiChapter 1 revisited
2013-02-11 Ferruccio Guidimore service lemmas in nat and lambdadelta
2013-02-07 Andrea AspertiA few integrations
2013-02-07 Andrea Aspertirestructuring
2013-02-07 Andrea Asperti(no commit message)
2013-02-07 Andrea Aspertirestructuring
2013-02-04 Wilmer Ricciottistate mte2 renamed to mte_acc
2013-02-04 Wilmer Ricciotticonverting certain basic machines to composed machines
2013-02-04 Wilmer Ricciottidefs.ma was never really used
2013-02-02 Claudio Sacerdoti... Makefile to extract to ocaml code.
2013-02-02 Claudio Sacerdoti... Oops, part of last commit (ocaml extraction implementation)
2013-02-01 Ferruccio Guidilambda finaly moved in lib
2013-02-01 Wilmer Ricciottimatch now only uses the new move operation
2013-01-29 Wilmer RicciottiSpeed-up in match.ma.
2013-01-29 Wilmer RicciottiProved old axiom.
2013-01-29 Wilmer RicciottiYippeee! Completes proof of soundness of the universal...
2013-01-28 Andrea Aspertiunistep!!!
2013-01-28 Andrea Aspertifunzioni ausiliarie
2013-01-28 Wilmer Ricciotticfg_in_table_to_tuple
2013-01-28 Wilmer Ricciottisem_copy_strict
2013-01-27 Wilmer Ricciottimany axioms and daemons removed
2013-01-27 Andrea Aspertiquasi finito
2013-01-27 Wilmer Ricciottiwell-foundedness done
2013-01-27 Andrea Aspertisem_exec_move completed
2013-01-27 Andrea Aspertialmost there
2013-01-26 Andrea AspertiA lot of changes
2013-01-25 Andrea AspertiSplitted unistep_aux
2013-01-25 Wilmer Ricciottistarted unistep
2013-01-25 Wilmer Ricciottiprogress in termination
2013-01-24 Wilmer Ricciottifinished semantics for termination of match machine
2013-01-24 Wilmer Ricciottiprogress
2013-01-24 Wilmer Ricciottiprogress
2013-01-23 Wilmer Ricciottiprogress
2013-01-22 Andrea Aspertitermination!
2013-01-22 Andrea AspertiUniversal machine
2013-01-22 Wilmer RicciottiRemoved all axioms in unistep_aux
2013-01-21 Wilmer Ricciottiremoved daemons
next