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

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

projects / helm.git / history

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

[helm.git] / components / tactics / declarative.ml

2006-11-27	Claudio Sacerdoti...	Declarative language ported to new auto (with Universes).	blob \| commitdiff \| raw
2006-11-23	Andrea Asperti	Modifications to auto due to the introduction of the...	blob \| commitdiff \| raw \| diff to current
2006-11-14	Claudio Sacerdoti...	library=1 in obtain _ = _ by _.	blob \| commitdiff \| raw \| diff to current
2006-10-12	Claudio Sacerdoti...	Bug fixed: the conversion was done with the wront argum...	blob \| commitdiff \| raw \| diff to current
2006-10-10	Claudio Sacerdoti...	Implemented:	blob \| commitdiff \| raw \| diff to current
2006-10-03	maiorino	Some declarative tactics did not allow the "done" optio...	blob \| commitdiff \| raw \| diff to current
2006-10-03	Claudio Sacerdoti...	Syntax of paramodulation parameters changed.	blob \| commitdiff \| raw \| diff to current
2006-09-08	Claudio Sacerdoti...	Bug fixed: "by ... we proved ... that is equivalent...	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	Automation enabled for declarative proofs. Cool.	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	"that is equivalent to" and "or equivalently" implement...	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	All the declarative tactics now have a more or less...	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	Declarative tactics for rewriting steps, elimination...	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	New declarative commands (ast, pretty-printing and...	blob \| commitdiff \| raw \| diff to current
2006-07-12	Claudio Sacerdoti...	Missing copyright added to tactics/declarative.ml*	blob \| commitdiff \| raw \| diff to current
2006-07-11	maiorino	First experimental version of the declarative proof...	blob \| commitdiff \| raw \| diff to current

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