]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/declarative.ml
when use_only_paramod is true do not calculate the universe for applicative reasoning
[helm.git] / helm / software / components / tactics / declarative.ml
2006-09-08 Claudio Sacerdoti... Bug fixed: "by ... we proved ... that is equivalent...
2006-07-27 maiorinoAutomation enabled for declarative proofs. Cool.
2006-07-27 maiorino"that is equivalent to" and "or equivalently" implement...
2006-07-27 maiorinoAll the declarative tactics now have a more or less...
2006-07-27 maiorinoDeclarative tactics for rewriting steps, elimination...
2006-07-27 maiorinoNew declarative commands (ast, pretty-printing and...
2006-07-12 Claudio Sacerdoti... Missing copyright added to tactics/declarative.ml*
2006-07-11 maiorinoFirst experimental version of the declarative proof...