| 2009-06-09 |
denes | Optimized weigths comparison, removed normalization
|
commit | commitdiff | tree |
| 2009-06-09 |
denes | Implemented substitution application and concatenation
|
commit | commitdiff | tree |
| 2009-06-05 |
denes | First tests for paramodulation (pretty printer, unification)
|
commit | commitdiff | tree |
| 2009-06-05 |
denes | Fix : wrong exception was catch in apply_subst
|
commit | commitdiff | tree |
| 2009-06-04 |
denes | First pretty printing functions
|
commit | commitdiff | tree |
| 2009-06-01 |
denes | First implementation of unification on foterms
|
commit | commitdiff | tree |
| 2009-06-01 |
denes | First functions on substitutions for unification
|
commit | commitdiff | tree |
| 2007-10-14 |
Cristian Armentano | Theorem sigma_p_knm changed into generic_iter_p_knm.
|
commit | commitdiff | tree |
| 2007-09-20 |
Cristian Armentano | Further simplifications to the main theorem about Euler...
|
commit | commitdiff | tree |
| 2007-09-19 |
Cristian Armentano | * Some simplifications to theorem in file totient1.ma.
|
commit | commitdiff | tree |
| 2007-09-18 |
Cristian Armentano | some theorems have been moved to more appropriate files...
|
commit | commitdiff | tree |
| 2007-09-17 |
Cristian Armentano | temporary changes, before the complete cancellation...
|
commit | commitdiff | tree |
| 2007-09-17 |
Cristian Armentano | simplified version of a theorem.
|
commit | commitdiff | tree |
| 2007-09-11 |
Cristian Armentano | some theorem names changed.
|
commit | commitdiff | tree |
| 2007-09-10 |
Cristian Armentano | other simplifications.
|
commit | commitdiff | tree |
| 2007-09-09 |
Cristian Armentano | other simplifications.
|
commit | commitdiff | tree |
| 2007-09-07 |
Cristian Armentano | some simplifications.
|
commit | commitdiff | tree |
| 2007-09-06 |
Cristian Armentano | Some simplifications.
|
commit | commitdiff | tree |
| 2007-08-16 |
Cristian Armentano | little change to theorem eq_gcd_times_times_eqv_times_gcd
|
commit | commitdiff | tree |
| 2007-07-30 |
Cristian Armentano | renamed generic_sigma_p.ma to generic_iter_p.ma
|
commit | commitdiff | tree |
| 2007-06-30 |
Cristian Armentano | New definition of Euler's totient function.
|
commit | commitdiff | tree |
| 2007-06-29 |
Cristian Armentano | generic version, specializing generic_sigma_p.ma
|
commit | commitdiff | tree |
| 2007-06-29 |
Cristian Armentano | generic version
|
commit | commitdiff | tree |
| 2007-06-29 |
Cristian Armentano | theorems about sigma_p proved using sigma_p_gen
|
commit | commitdiff | tree |
| 2007-06-27 |
Cristian Armentano | new gcd properties, and theorems for totient, and theorems...
|
commit | commitdiff | tree |
| 2007-06-26 |
Cristian Armentano | (no commit message)
|
commit | commitdiff | tree |
| 2007-06-26 |
Cristian Armentano | generic sommatory.
|
commit | commitdiff | tree |
| 2007-05-18 |
lzingare | added alternative implementation for hMysql relying
|
commit | commitdiff | tree |
| 2007-04-20 |
Cristian Armentano | changed base uri
|
commit | commitdiff | tree |
| 2007-04-20 |
Cristian Armentano | initial import
|
commit | commitdiff | tree |
| 2007-03-01 |
Enrico Zoli | "by j let x : T such that P(x)" generalized to allow...
|
commit | commitdiff | tree |
| 2007-02-20 |
notin | small fix to make it compile again
|
commit | commitdiff | tree |
| 2007-01-17 |
Enrico Zoli | This is the roadmap of the constructive proof of Lebesgue...
|
commit | commitdiff | tree |
| 2006-12-15 |
Enrico Zoli | Up to definition of limsup as liminf computed on the...
|
commit | commitdiff | tree |
| 2006-12-15 |
Enrico Zoli | Fatou lemma achieved (up to a few more axioms here...
|
commit | commitdiff | tree |
| 2006-11-14 |
maiorino | New: on-line help for declarative tactics (first version).
|
commit | commitdiff | tree |
| 2006-11-10 |
Enrico Zoli | Dama: up to L-spaces and the proof (completed up to...
|
commit | commitdiff | tree |
| 2006-11-06 |
Enrico Zoli | More work on groups, real numbers and integration algebras.
|
commit | commitdiff | tree |
| 2006-11-03 |
Enrico Zoli | Integration f_algebras declassed.
|
commit | commitdiff | tree |
| 2006-11-03 |
Enrico Zoli | Up to absolute value
|
commit | commitdiff | tree |
| 2006-11-03 |
Enrico Zoli | Up to max (up to a bug).
|
commit | commitdiff | tree |
| 2006-10-31 |
Enrico Zoli | We begin to play the real game: we have defined real...
|
commit | commitdiff | tree |
| 2006-10-31 |
Enrico Zoli | Integration_algebras.ma split into 6 different files.
|
commit | commitdiff | tree |
| 2006-10-31 |
Enrico Zoli | Syntax changed (to be changed back) for left parameters...
|
commit | commitdiff | tree |
| 2006-10-24 |
Enrico Zoli | Added unit to rings.
|
commit | commitdiff | tree |
| 2006-10-24 |
Enrico Zoli | More coercions added in the algebraic hierarchy.
|
commit | commitdiff | tree |
| 2006-10-24 |
Enrico Zoli | Up to f_algebras.
|
commit | commitdiff | tree |
| 2006-10-20 |
Enrico Zoli | Up to f_algebras.
|
commit | commitdiff | tree |
| 2006-10-20 |
Enrico Zoli | 1. developed up to algebras
|
commit | commitdiff | tree |
| 2006-10-20 |
Enrico Zoli | Serious bug fixed: without a Lazy.force the user obtained...
|
commit | commitdiff | tree |
| 2006-10-16 |
Enrico Zoli | Beginning of the development of integration algebras.
|
commit | commitdiff | tree |
| 2006-10-12 |
acciavat | auto => auto new.
|
commit | commitdiff | tree |
| 2006-10-12 |
acciavat | Manual porting of CoRN to Matita.
|
commit | commitdiff | tree |
| 2006-10-03 |
maiorino | Some declarative tactics did not allow the "done" option...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | Automation enabled for declarative proofs. Cool.
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | "that is equivalent to" and "or equivalently" implemented...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | All the declarative tactics now have a more or less...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | Declarative tactics for rewriting steps, elimination...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | Notation for the existential quantifier moved to core_notati...
|
commit | commitdiff | tree |
| 2006-07-27 |
maiorino | New declarative commands (ast, pretty-printing and...
|
commit | commitdiff | tree |
| 2006-07-11 |
maiorino | First experimental version of the declarative proof...
|
commit | commitdiff | tree |
| 2006-03-10 |
marangon | Added inversion principle creation for inductive predicates.
|
commit | commitdiff | tree |
| 2006-03-10 |
marangon | Inversion code cleaning.
|
commit | commitdiff | tree |
| 2006-03-03 |
marangon | PP of Refine.RefineFailure.
|
commit | commitdiff | tree |
| 2006-01-11 |
marangon | Code clean up.
|
commit | commitdiff | tree |
| 2005-12-15 |
marangon | New tactic: inversion.
|
commit | commitdiff | tree |
| 2005-12-15 |
marangon | New tactic: inversion.
|
commit | commitdiff | tree |
| 2005-12-15 |
marangon | ...
|
commit | commitdiff | tree |
| 2005-12-15 |
marangon | added -I ../.. (for coq.ma)
|
commit | commitdiff | tree |
| 2004-03-31 |
Lionel Mamane | Meta files are in METAS subdir
|
commit | commitdiff | tree |
| 2004-03-31 |
Lionel Mamane | Install to findlib-defined dest dir, not to stdlib dir
|
commit | commitdiff | tree |
| 2004-03-12 |
acerioni | New tactic Auto.
|
commit | commitdiff | tree |
| 2004-03-12 |
acerioni | First implementation of the Auto tactic.
|
commit | commitdiff | tree |
| 2004-03-12 |
acerioni | Type of exception changed: from exn to string.
|
commit | commitdiff | tree |
| 2003-09-09 |
pmasoudi | snapshot
|
commit | commitdiff | tree |
| 2003-09-08 |
pmasoudi | select and click signal added
|
commit | commitdiff | tree |
| 2003-09-04 |
pmasoudi | scrollbars added & control structure screated
|
commit | commitdiff | tree |
| 2003-07-31 |
pmasoudi | * added first version of persist stream implementation...
|
commit | commitdiff | tree |
| 2003-07-17 |
pmasoudi | Partional first fase final.
|
commit | commitdiff | tree |
| 2003-07-17 |
pmasoudi | Persist file completed.
|
commit | commitdiff | tree |
| 2003-07-16 |
pmasoudi | Control Factory modified.
|
commit | commitdiff | tree |
| 2003-07-16 |
pmasoudi | persist file with factory.
|
commit | commitdiff | tree |
| 2003-07-16 |
pmasoudi | added persit-file-implementation.
|
commit | commitdiff | tree |
| 2002-11-27 |
natile | objectName patched.
|
commit | commitdiff | tree |
| 2002-11-27 |
natile | Relation patched, property added.
|
commit | commitdiff | tree |
| 2002-11-22 |
natile | Debugging prints removed.
|
commit | commitdiff | tree |
| 2002-11-22 |
natile | Mathql_interpreter now using db helm_mowgli_new_schema.
|
commit | commitdiff | tree |
| 2002-11-19 |
natile | Now Pattern module really exists in repository.
|
commit | commitdiff | tree |
| 2002-11-19 |
natile | Pattern module added.
|
commit | commitdiff | tree |
| 2002-11-18 |
natile | Relation: inverse switch added.
|
commit | commitdiff | tree |
| 2002-11-14 |
natile | Attribute files added.
|
commit | commitdiff | tree |
| 2002-11-14 |
natile | Unused files removed.
|
commit | commitdiff | tree |
| 2002-11-13 |
natile | Attribute patched: now takes an extra argument of type...
|
commit | commitdiff | tree |
| 2002-11-13 |
natile | Attribute patched with inverse function.
|
commit | commitdiff | tree |
| 2002-11-04 |
natile | Fun patched.
|
commit | commitdiff | tree |
| 2002-10-28 |
natile | Fun patched but works only in one direction (from the...
|
commit | commitdiff | tree |
| 2002-10-22 |
natile | Switching interpreter patched, addedd:
|
commit | commitdiff | tree |
| 2002-10-21 |
natile | Old modules (use.ml/mli, eval.ml/mli,...) eliminated.
|
commit | commitdiff | tree |
| 2002-10-21 |
natile | Switching interpreter.
|
commit | commitdiff | tree |
| 2002-10-21 |
Michele Galatà | Comments reindented.
|
commit | commitdiff | tree |
| next |
projects / helm.git / search