]> matita.cs.unibo.it Git - helm.git/history - matita/library
new file with some relations stated in Type
[helm.git] / matita / library /
2007-11-08 Enrico Tassiported to the new destruct
2007-11-06 Ferruccio Guidinew implementation of the destruct tactic,
2007-10-28 Claudio Sacerdoti... Nil => nil, Cons => cons
2007-10-28 Claudio Sacerdoti... Nil => nil; Cons => cons
2007-10-28 Claudio Sacerdoti... New syntax for match patterns.
2007-10-25 Claudio Sacerdoti... neg => Qneg :-)
2007-10-25 Claudio Sacerdoti... true and false were swapped!
2007-10-25 Claudio Sacerdoti... flase => false :-)
2007-10-16 Claudio Sacerdoti... Interesting. Do we need many more inversion lemmas...
2007-10-14 Claudio Sacerdoti... Caseness problems fixed.
2007-10-14 Claudio Sacerdoti... Some lemmas moves to the file they belong to.
2007-10-14 Cristian ArmentanoTheorem sigma_p_knm changed into generic_iter_p_knm.
2007-10-12 Claudio Sacerdoti... Move to OCaml 3.10. Requires debian packages from unsta...
2007-10-12 Wilmer RicciottiFixed baseuri
2007-10-12 Wilmer RicciottiPart1a update...
2007-10-12 Andrea AspertiMore restructuring in moebius.ma
2007-10-12 Andrea AspertiReorganization of the library.
2007-10-12 Andrea AspertiReorganization of the library.
2007-10-12 Andrea AspertiReorganization of results.
2007-10-08 Andrea AspertiSome axioms for Q.
2007-09-24 Wilmer RicciottiLast version of poplmark 1a, featuring new proof, only...
2007-09-20 Cristian ArmentanoFurther simplifications to the main theorem about Euler...
2007-09-19 Cristian Armentano* Some simplifications to theorem in file totient1.ma.
2007-09-18 Cristian Armentanosome theorems have been moved to more appropriate files...
2007-09-17 Cristian Armentanotemporary changes, before the complete cancellation...
2007-09-17 Cristian Armentanosimplified version of a theorem.
2007-09-17 Andrea AspertiSome new lemmas.
2007-09-17 Andrea AspertiA new function.
2007-09-14 Andrea AspertiQualche semplificazione.
2007-09-12 Wilmer RicciottiUpdated, proofs are now about 750 lines.
2007-09-11 Cristian Armentanosome theorem names changed.
2007-09-10 Cristian Armentanoother simplifications.
2007-09-09 Enrico Tassi...
2007-09-09 Cristian Armentanoother simplifications.
2007-09-08 Enrico Tassi...
2007-09-07 Cristian Armentanosome simplifications.
2007-09-06 Cristian ArmentanoSome simplifications.
2007-08-30 Enrico Tassimore stuff to reach an intensional definition of finite...
2007-08-28 Claudio Sacerdoti... * definition of implication free propositional formulas
2007-08-16 Cristian Armentanolittle change to theorem eq_gcd_times_times_eqv_times_gcd
2007-07-31 Andrea Aspertiremoved generic_sigma_p since generic_iter_p is the...
2007-07-31 Enrico Tassisomething was really too slow...
2007-07-30 Cristian Armentanorenamed generic_sigma_p.ma to generic_iter_p.ma
2007-07-26 Wilmer RicciottiSome notation added
2007-07-25 Enrico Tassiadded some notation
2007-07-23 Claudio Sacerdoti... Prototype of min_aux changed.
2007-07-20 Claudio Sacerdoti... Another nicer version.
2007-07-20 Claudio Sacerdoti... Even nicer script.
2007-07-20 Claudio Sacerdoti... The nicest script obtained so far.
2007-07-20 Claudio Sacerdoti... More simplification due to the new conversion strategy.
2007-07-20 Claudio Sacerdoti... Script simplification due to the new efficient conversi...
2007-07-19 Claudio Sacerdoti... Super-nice notation for the assembly stuff.
2007-07-17 Claudio Sacerdoti... added missing parenthesis
2007-07-17 Enrico Tassifixed includes and added notation for bytes
2007-07-16 Claudio Sacerdoti... More lemmas.
2007-07-16 Claudio Sacerdoti... More daemons closed. A couple left in byte and many...
2007-07-16 Claudio Sacerdoti... More daemons/axioms closed.
2007-07-16 Claudio Sacerdoti... One daemon less.
2007-07-16 Claudio Sacerdoti... More daemons got rid of (and more extra axioms to be...
2007-07-16 Claudio Sacerdoti... Last daemon killed :-)
2007-07-16 Claudio Sacerdoti... One less daemon (about "update"s).
2007-07-16 Claudio Sacerdoti... All sub-proofs about "update" closed.
2007-07-16 Claudio Sacerdoti... assembly.ma splitted into many files
2007-07-16 Wilmer Ricciotticorrected axiom mod_plus
2007-07-13 Claudio Sacerdoti... More conjectures closed.
2007-07-13 Claudio Sacerdoti... 1. requires the new pretty printer for natural numbers
2007-07-13 Claudio Sacerdoti... Final theorem proved. Many many conjectures left. I...
2007-07-12 Claudio Sacerdoti... The loop invariant I chosed was not correct!
2007-07-11 Claudio Sacerdoti... Getting close to the final result.
2007-07-11 Claudio Sacerdoti... 1. loop invariant stated, but not proved
2007-07-11 Claudio Sacerdoti... 1. status factorized out in tick
2007-07-10 Claudio Sacerdoti... 0. less nice solution by Enrico reverted
2007-07-10 Enrico TassiLa programmazione funzionale e' come TeX, funziona...
2007-07-09 Enrico Tassi1. bug fixed in tick
2007-07-09 Claudio Sacerdoti... Interesting theorem added (but still to be proved).
2007-07-07 Enrico Tassiinclusion of div_and_mod
2007-07-06 Enrico Tassimaxipatch for support of multiple DBs.
2007-07-05 Claudio Sacerdoti... Exadecimal numbers are now used. This is a great speed-up.
2007-07-04 Claudio Sacerdoti... Example program executed for x,y=0.
2007-07-04 Claudio Sacerdoti... Quick hack: matita natural numbers are now accepted...
2007-07-04 Claudio Sacerdoti... More opcodes (badly) implemented.
2007-07-04 Claudio Sacerdoti... List.ma: added function nth (with default value in...
2007-06-30 Cristian ArmentanoNew definition of Euler's totient function.
2007-06-29 Cristian Armentanogeneric version, specializing generic_sigma_p.ma
2007-06-29 Cristian Armentanogeneric version
2007-06-29 Cristian Armentanotheorems about sigma_p proved using sigma_p_gen
2007-06-27 Cristian Armentanonew gcd properties, and theorems for totient, and theor...
2007-06-26 Cristian Armentano(no commit message)
2007-06-26 Cristian Armentanogeneric sommatory.
2007-06-21 Wilmer RicciottiPoplMark challenge part 1a: new, shorter version w...
2007-05-24 Enrico Tassiauto and autogui... some work
2007-05-20 Ferruccio GuidiapplyTransformation: added debugging information
2007-05-17 Enrico Tassiauto rewritten with only one tail recursive function.
2007-05-09 Andrea AspertiA few extensions for the moebius inversion theorem
2007-05-09 Andrea AspertiProof of the moebius inversion theorem
2007-04-20 Claudio Sacerdoti... Much ado about nothing:
2007-04-18 Enrico Tassimore discriminate
2007-04-16 Enrico Tassibetter simplify
2007-04-16 Enrico Tassiclosed all axioms
2007-04-10 Enrico Tassiset -> type
next