| 2005-11-22 |
Claudio Sacerdoti... | Last details. |
tree | commitdiff |
| 2005-11-21 |
Claudio Sacerdoti... | Proof using function induction terminated. It's really... |
tree | commitdiff |
| 2005-11-21 |
Claudio Sacerdoti... | Lost of redundant typing hints removed from the functio... |
tree | commitdiff |
| 2005-11-21 |
Claudio Sacerdoti... | New proof based on an hand-made functional induction. |
tree | commitdiff |
| 2005-11-21 |
Claudio Sacerdoti... | Useful lemma added. |
tree | commitdiff |
| 2005-11-16 |
Claudio Sacerdoti... | New framework for regression of bad tests. |
tree | commitdiff |
| 2005-11-08 |
Claudio Sacerdoti... | Yet another semantics for simplify. |
tree | commitdiff |
| 2005-11-07 |
Claudio Sacerdoti... | Syntactic change: |
tree | commitdiff |
| 2005-11-07 |
Stefano Zacchiroli | list sorting (to be completed ...) |
tree | commitdiff |
| 2005-11-07 |
Stefano Zacchiroli | added tail function |
tree | commitdiff |
| 2005-11-07 |
Stefano Zacchiroli | added bool_elim (elimination which preserves infos... |
tree | commitdiff |
| 2005-11-04 |
Enrico Tassi | since the outtype is now refined correclty some types... |
tree | commitdiff |
| 2005-11-03 |
Andrea Asperti | Euler totient function is multiplicative! |
tree | commitdiff |
| 2005-11-02 |
Claudio Sacerdoti... | Unfinished proof commented out. |
tree | commitdiff |
| 2005-11-02 |
Claudio Sacerdoti... | Proof of unicity of proofs for: |
tree | commitdiff |
| 2005-11-02 |
Enrico Tassi | () around tactic terms |
tree | commitdiff |
| 2005-11-02 |
Andrea Asperti | Totient function and related files. |
tree | commitdiff |
| 2005-10-25 |
Claudio Sacerdoti... | Parentheses must now be put in patterns like in tactic... |
tree | commitdiff |
| 2005-10-25 |
Stefano Zacchiroli | ported to new syntactic requirement about terms being... |
tree | commitdiff |
| 2005-10-06 |
Stefano Zacchiroli | bugfix: avoid diversion in "make opt" |
tree | commitdiff |
| 2005-10-05 |
Stefano Zacchiroli | separated "]]" to avoid clash with (temporary) continua... |
tree | commitdiff |
| 2005-10-05 |
Stefano Zacchiroli | added MATITA_FLAGS support |
tree | commitdiff |
| 2005-10-03 |
Andrea Asperti | Added congruence.ma. |
tree | commitdiff |
| 2005-10-03 |
Andrea Asperti | Several changes. Proof of Fermat's little theorem compl... |
tree | commitdiff |
| 2005-09-29 |
Stefano Zacchiroli | moved a (commented) test in a handier position |
tree | commitdiff |
| 2005-09-28 |
Andrea Asperti | New entry: relevant_equations. |
tree | commitdiff |
| 2005-09-28 |
Stefano Zacchiroli | spotted missing times notation |
tree | commitdiff |
| 2005-09-27 |
Andrea Asperti | small error in nth_prime. |
tree | commitdiff |
| 2005-09-27 |
Andrea Asperti | New entry: fermat's little theorem (almost complete). |
tree | commitdiff |
| 2005-09-27 |
Stefano Zacchiroli | completed use of \mod and / notation |
tree | commitdiff |
| 2005-09-26 |
Stefano Zacchiroli | function composition notation |
tree | commitdiff |
| 2005-09-26 |
Stefano Zacchiroli | div and mod notation ('%' and '\mod') |
tree | commitdiff |
| 2005-09-26 |
Claudio Sacerdoti... | Unification enhanchement. |
tree | commitdiff |
| 2005-09-26 |
Andrea Asperti | permutation.ma added to the repository. |
tree | commitdiff |
| 2005-09-26 |
Stefano Zacchiroli | better name for a theorem |
tree | commitdiff |
| 2005-09-23 |
Andrea Asperti | log.ma renamed into ord.ma |
tree | commitdiff |
| 2005-09-23 |
Andrea Asperti | A few changes to factorization and gcd. |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | More notation here and there. |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | More notation here and there: \sup, \divides, \ndivides, ! |
tree | commitdiff |
| 2005-09-22 |
Claudio Sacerdoti... | More notation here and there. |
tree | commitdiff |
| 2005-09-21 |
Stefano Zacchiroli | uses ligatures (as a sample) |
tree | commitdiff |
| 2005-09-20 |
Stefano Zacchiroli | added non-builtin notation for exists |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | * Obsolete debugging comments removed |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Notation for "ex" introduced. It is the same as the... |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Spurious interpretation removed. |
tree | commitdiff |
| 2005-09-19 |
Stefano Zacchiroli | added list.ma |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Removed final question marks from {apply|elim|rewrite}s. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | Some code that used to avoid a fixed bug removed. |
tree | commitdiff |
| 2005-09-19 |
Claudio Sacerdoti... | .ma inclusions corrected/minimized |
tree | commitdiff |
| 2005-09-16 |
Enrico Tassi | added a function to reorder the metasenv. |
tree | commitdiff |
| 2005-09-16 |
Stefano Zacchiroli | added notation for nleq, nlgt, ... |
tree | commitdiff |
| 2005-09-15 |
Claudio Sacerdoti... | "bool.ma" is now always included before "logic.ma"... |
tree | commitdiff |
| 2005-09-15 |
Stefano Zacchiroli | added \neq notation |
tree | commitdiff |
| 2005-09-14 |
Andrea Asperti | Product, pair and projections. |
tree | commitdiff |
| 2005-09-14 |
Andrea Asperti | factorization.ma |
tree | commitdiff |
| 2005-09-14 |
Andrea Asperti | New version of the library. nth_prime, gcd, log. |
tree | commitdiff |
| 2005-09-13 |
Stefano Zacchiroli | fixed parsing of --x=x ("'uminus" is now right associative) |
tree | commitdiff |
| 2005-09-13 |
Stefano Zacchiroli | removed a comment/bug report about let..in rendering... |
tree | commitdiff |
| 2005-09-12 |
Stefano Zacchiroli | removed work-arounds for poor disambiguation, which... |
tree | commitdiff |
| 2005-09-12 |
Claudio Sacerdoti... | Comment removed. |
tree | commitdiff |
| 2005-08-22 |
Andrea Asperti | Added datatypes/constructors.ma |
tree | commitdiff |
| 2005-08-22 |
Andrea Asperti | New entries in nat: factorial.ma minimization.ma primes... |
tree | commitdiff |
| 2005-08-22 |
Andrea Asperti | Added Z/plus.ma e Z/compare.ma. |
tree | commitdiff |
| 2005-08-22 |
Andrea Asperti | The library grows... |
tree | commitdiff |
| 2005-08-22 |
Andrea Asperti | Added q.ma. |
tree | commitdiff |
| 2005-07-28 |
Andrea Asperti | removed orders_op from library (now in le_arith and... |
tree | commitdiff |
| 2005-07-28 |
Claudio Sacerdoti... | Committing all the recent development of Andrea after... |
tree | commitdiff |
| 2005-07-28 |
Claudio Sacerdoti... | More notation. |
tree | commitdiff |
| 2005-07-26 |
Claudio Sacerdoti... | **** Experimental: **** |
tree | commitdiff |
| 2005-07-25 |
Claudio Sacerdoti... | More notation (up to where the open bugs allow me to... |
tree | commitdiff |
| 2005-07-25 |
Claudio Sacerdoti... | A little bit more of notation here and there. |
tree | commitdiff |
| 2005-07-25 |
Claudio Sacerdoti... | Notation for equality used everywhere. |
tree | commitdiff |
| 2005-07-22 |
Claudio Sacerdoti... | Big changes: |
tree | commitdiff |
| 2005-07-21 |
Claudio Sacerdoti... | S_pred moved from Z/times.ma to nat/orders.ma |
tree | commitdiff |
| 2005-07-19 |
Claudio Sacerdoti... | Many bugs in the Makefile fixed. |
tree | commitdiff |
| 2005-07-19 |
Andrea Asperti | New naming policy for local variables. |
tree | commitdiff |
| 2005-07-19 |
Enrico Tassi | avoids generating a wrong/empty/dummy depend |
tree | commitdiff |
| 2005-07-15 |
Andrea Asperti | Added a new contrib div_and_mod and few modifs here... |
tree | commitdiff |
| 2005-07-13 |
Enrico Tassi | use dvariant for associtivity |
tree | commitdiff |
| 2005-07-13 |
Enrico Tassi | removed drop. |
tree | commitdiff |
| 2005-07-13 |
Andrea Asperti | New version of the library. |
tree | commitdiff |
| 2005-07-11 |
Claudio Sacerdoti... | A few .cvsignore here and there. |
tree | commitdiff |
| 2005-07-11 |
Claudio Sacerdoti... | Bug fixed: the generated elimination principles used... |
tree | commitdiff |
| 2005-07-11 |
Andrea Asperti | only regular files are ending in .ma are now searched |
tree | commitdiff |
| 2005-07-11 |
Andrea Asperti | New version of the library, a bit more structured. |
tree | commitdiff |
| 2005-07-11 |
Andrea Asperti | Removed the old library. |
tree | commitdiff |
| 2005-07-08 |
Claudio Sacerdoti... | dead code removed |
tree | commitdiff |
| 2005-07-08 |
Claudio Sacerdoti... | 1. PrimitiveTactics.new_metasenv_for_apply changed... |
tree | commitdiff |
| 2005-07-07 |
Claudio Sacerdoti... | No more need for symbolic links: .matita, the configura... |
tree | commitdiff |
| 2005-07-07 |
Claudio Sacerdoti... | matitaclean now removes the .moo file, if existent. |
tree | commitdiff |
| 2005-07-07 |
Enrico Tassi | fixed according to the new fresh name generator |
tree | commitdiff |
| 2005-07-07 |
Claudio Sacerdoti... | matita.ma.templ must be symbolically linked |
tree | commitdiff |
| 2005-07-06 |
Claudio Sacerdoti... | 1. tactical "try_tacticals" renamed to "first" |
tree | commitdiff |
| 2005-07-05 |
Claudio Sacerdoti... | let's find the .ma files also in subdirectories |
tree | commitdiff |
| 2005-07-05 |
Claudio Sacerdoti... | re-added $(H) to matitaclean |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | icons added to the list of required symbolic links |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | make clean now prints what is being removed |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | New command default "foo" uri1 ... urin |
tree | commitdiff |
| 2005-07-04 |
Enrico Tassi | moo do not depend on .depend |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | "include" command implemented. |
tree | commitdiff |
| next |
projects / helm.git / history