matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/autoTactic.ml

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/autoTactic.ml

projects / helm.git / history

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

[helm.git] / helm / software / components / tactics / autoTactic.ml

2006-10-06	Enrico Tassi	resumed ol auto	blob \| commitdiff \| raw
2006-10-02	Enrico Tassi	auto always uses the context (even if paramodulation...	blob \| commitdiff \| raw \| diff to current
2006-10-01	Enrico Tassi	when use_only_paramod is true do not calculate the...	blob \| commitdiff \| raw \| diff to current
2006-09-29	Enrico Tassi	new version of auto that is able to prove the irrationa...	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-24	Enrico Tassi	added timeout parameter to auto paramodulation.	blob \| commitdiff \| raw \| diff to current
2006-07-22	Enrico Tassi	matitaprover	blob \| commitdiff \| raw \| diff to current
2006-06-27	Enrico Tassi	using the new metadataConstraint function	blob \| commitdiff \| raw \| diff to current
2006-06-26	Enrico Tassi	more work for the generic auto parameters	blob \| commitdiff \| raw \| diff to current
2006-06-21	Enrico Tassi	added the geniric	blob \| commitdiff \| raw \| diff to current
2006-06-15	Andrea Asperti	added applyS	blob \| commitdiff \| raw \| diff to current
2006-05-31	Enrico Tassi	fixed proofs, contextualization should now work.	blob \| commitdiff \| raw \| diff to current
2006-05-29	Enrico Tassi	profilings are printed	blob \| commitdiff \| raw \| diff to current
2006-04-26	Enrico Tassi	added a new type for proofs.	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.