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 |
2005-07-04 |
Enrico Tassi | matitaclean now call getter.ls using a buri with a... |
tree | commitdiff |
2005-07-03 |
Claudio Sacerdoti... | Equality tactics are now used in the first half of... |
tree | commitdiff |
2005-07-02 |
Claudio Sacerdoti... | The equality tactics are now exploited. |
tree | commitdiff |
2005-07-02 |
Claudio Sacerdoti... | New theorem: eq_ind_r. |
tree | commitdiff |
2005-07-02 |
Claudio Sacerdoti... | cosmetic change: a space removed (to make tests/Makefil... |
tree | commitdiff |
2005-07-01 |
Enrico Tassi | more makefile work |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | matitaclean is necessary! |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | * makefile improved |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | new targets: |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | make all is now nicer |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | Two targets now: |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | make MATITAC="../scripts/do_tests.sh ../matitac /dev... |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | Makefile improved |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | The library of matita is borned! Long life to the libra... |
tree | commitdiff |
|