matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/paramodulation/indexing.mli

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/paramodulation/indexing.mli

[helm.git] / helm / software / components / tactics / paramodulation / indexing.mli

2009-06-25	Enrico Tassi	initial import of standalone matitaprover binary	blob \| commitdiff \| raw
2009-05-06	Enrico Tassi	apply and auto.equational_case call saturation.solve_na...	blob \| commitdiff \| raw \| diff to current
2009-04-28	Enrico Tassi	huge commit in automation:	blob \| commitdiff \| raw \| diff to current
2009-04-20	Enrico Tassi	- init_cache_and_tables rewritten using the automation_...	blob \| commitdiff \| raw \| diff to current
2008-10-29	Andrea Asperti	New demod function working for arbitary goals.	blob \| commitdiff \| raw \| diff to current
2008-09-19	Enrico Tassi	more abstract discrimination tree	blob \| commitdiff \| raw \| diff to current
2008-09-19	Enrico Tassi	better abstraction to allow 1 discrimination tree imple...	blob \| commitdiff \| raw \| diff to current
2008-09-19	Andrea Asperti	A temporary patch to demodulation theorem.	blob \| commitdiff \| raw \| diff to current
2007-06-13	Enrico Tassi	many changes:	blob \| commitdiff \| raw \| diff to current
2006-10-20	Andrea Asperti	Major changes to auto, documented on the helm mailing...	blob \| commitdiff \| raw \| diff to current
2006-09-27	Enrico Tassi	auto snapshot	blob \| commitdiff \| raw \| diff to current
2006-09-21	Enrico Tassi	auto snapshot	blob \| commitdiff \| raw \| diff to current
2006-07-11	Enrico Tassi	- removed Positive and Negative (all is positive)	blob \| commitdiff \| raw \| diff to current
2006-06-29	Enrico Tassi	goals after a superposition step are relocated	blob \| commitdiff \| raw \| diff to current
2006-06-18	Enrico Tassi	- some fixes regarding URIs of equality that now should...	blob \| commitdiff \| raw \| diff to current
2006-05-30	Enrico Tassi	fixed proof generation again	blob \| commitdiff \| raw \| diff to current
2006-05-29	Enrico Tassi	- proofs by subsumption now add a symmetry step if...	blob \| commitdiff \| raw \| diff to current
2006-05-22	Enrico Tassi	- code cleanup, especialli in Indexing where all the...	blob \| commitdiff \| raw \| diff to current
2006-05-20	Enrico Tassi	fixed demodulation of goal	blob \| commitdiff \| raw \| diff to current
2006-05-15	Enrico Tassi	- new given_clause	blob \| commitdiff \| raw \| diff to current
2006-05-14	Enrico Tassi	- Removed old proofs	blob \| commitdiff \| raw \| diff to current
2006-04-26	Enrico Tassi	added a new type for proofs.	blob \| commitdiff \| raw \| diff to current
2006-04-05	Enrico Tassi	the tactic now returns as open goals the open metas...	blob \| commitdiff \| raw \| diff to current
2006-04-04	Andrea Asperti	Naif substitution. Removed local context in metas durin...	blob \| commitdiff \| raw \| diff to current
2006-03-27	Andrea Asperti	args removed from equalities.	blob \| commitdiff \| raw \| diff to current
2006-03-20	Andrea Asperti	Snapshot.	blob \| commitdiff \| raw \| diff to current
2006-02-03	Stefano Zacchiroli	- renamed ocaml/ to components/	blob \| commitdiff \| raw \| diff to current

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

RSS Atom