matita.cs.unibo.it Git - helm.git/history - helm/ocaml/paramodulation/saturate

]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/paramodulation/saturate_main.ml

[helm.git] / helm / ocaml / paramodulation / saturate_main.ml

2006-01-12	Andrea Asperti	Moved paramodulation inside tactics.	commit \| commitdiff
2006-01-09	Andrea Asperti	ignoring the result of load_notation	commit \| commitdiff
2006-01-09	Andrea Asperti	Added a parameter (empty list) to load_notation.	commit \| commitdiff
2006-01-08	Claudio Sacerdoti...	Added $Id$ to every .ml file.	commit \| commitdiff
2005-12-19	Andrea Asperti	Discrimination and trie removed.	commit \| commitdiff
2005-12-06	Stefano Zacchiroli	bugfixes:	commit \| commitdiff
2005-12-05	Alberto Griggio	added function saturate_equations that tries to infer...	commit \| commitdiff
2005-11-25	Stefano Zacchiroli	changed META dependency	commit \| commitdiff
2005-10-25	Andrea Asperti	experimental version	commit \| commitdiff
2005-10-17	Alberto Griggio	added some comments; general code cleanup	commit \| commitdiff
2005-10-10	Alberto Griggio	fixed a bug (status not reset properly between calls...	commit \| commitdiff
2005-09-29	Alberto Griggio	upgraded code to work with non-default equalities	commit \| commitdiff
2005-09-26	Alberto Griggio	new paramodulation	commit \| commitdiff
2005-09-23	Claudio Sacerdoti...	New module HMysql (to abstract over Mysql and make...	commit \| commitdiff
2005-09-21	Alberto Griggio	bugfix on proof construction	commit \| commitdiff
2005-09-01	Alberto Griggio	changed default parameter values...	commit \| commitdiff
2005-08-22	Alberto Griggio	some fixes	commit \| commitdiff
2005-08-05	Alberto Griggio	some bugs fixed	commit \| commitdiff
2005-07-21	Alberto Griggio	added CicNotation.load_notation call to disambiguate...	commit \| commitdiff
2005-07-21	Alberto Griggio	entry point of the stand-alone saturate	commit \| commitdiff

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom