]> matita.cs.unibo.it Git - helm.git/commit
Declarative tactics for rewriting steps, elimination of the existential
authormaiorino <??>
Thu, 27 Jul 2006 14:47:57 +0000 (14:47 +0000)
committermaiorino <??>
Thu, 27 Jul 2006 14:47:57 +0000 (14:47 +0000)
commit36243ef64310a9ea2e51a0295744ab5de7abe055
tree5cb01271ba4afc6851f7c5f7b744a915054ee35b
parent4c64aae84bbfd12abb64e7af5a640192b5051dc3
Declarative tactics for rewriting steps, elimination of the existential
quantifier and elimination of conjunciton implemented.
components/grafite/grafiteAst.ml
components/grafite/grafiteAstPp.ml
components/grafite_engine/grafiteEngine.ml
components/grafite_parser/grafiteDisambiguate.ml
components/grafite_parser/grafiteParser.ml
components/tactics/declarative.ml
components/tactics/declarative.mli
matita/matita.lang
matita/tests/decl.ma