]> matita.cs.unibo.it Git - helm.git/commit
First implementation of the Auto tactic.
authoracerioni <??>
Fri, 12 Mar 2004 09:54:38 +0000 (09:54 +0000)
committeracerioni <??>
Fri, 12 Mar 2004 09:54:38 +0000 (09:54 +0000)
commitf654787b2156ede958a1d35ca8daf239de1b7b89
tree8b7b2085e35aef3cc7e2a33d7c4567c177ba4c84
parent5ce3527a194c90e1c4c9073afbb3863412304048
First implementation of the Auto tactic.
- tacticChaser: added a function to locate all the theorem tha can be applied
- variousTactics: the Auto tactic
helm/ocaml/tactics/.depend
helm/ocaml/tactics/Makefile
helm/ocaml/tactics/tacticChaser.ml
helm/ocaml/tactics/tacticChaser.mli
helm/ocaml/tactics/variousTactics.ml
helm/ocaml/tactics/variousTactics.mli