]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/tactics/
added support for goal patterns
[helm.git] / helm / ocaml / tactics /
drwxr-xr-x   ..
-rw-r--r-- 59 .cvsignore
-rw-r--r-- 5932 .depend
-rw-r--r-- 827 Makefile
-rw-r--r-- 12843 autoTactic.ml
-rw-r--r-- 1164 autoTactic.mli
-rw-r--r-- 29923 discriminationTactics.ml
-rw-r--r-- 1220 discriminationTactics.mli
-rw-r--r-- 8025 eliminationTactics.ml
-rw-r--r-- 1345 eliminationTactics.mli
-rw-r--r-- 7769 equalityTactics.ml
-rw-r--r-- 1677 equalityTactics.mli
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 1088 fourier.mli
-rw-r--r-- 43263 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 3453 fwdSimplTactic.ml
-rw-r--r-- 1232 fwdSimplTactic.mli
-rw-r--r-- 20064 hashtbl_equiv.ml
-rw-r--r-- 1690 hashtbl_equiv.mli
-rw-r--r-- 2985 history.ml
-rw-r--r-- 1147 history.mli
-rw-r--r-- 1958 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 19514 metadataQuery.ml
-rw-r--r-- 2085 metadataQuery.mli
-rw-r--r-- 3045 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
-rw-r--r-- 24701 primitiveTactics.ml
-rw-r--r-- 2117 primitiveTactics.mli
-rw-r--r-- 6113 proofEngineHelpers.ml
-rw-r--r-- 1883 proofEngineHelpers.mli
-rw-r--r-- 32479 proofEngineReduction.ml
-rw-r--r-- 1899 proofEngineReduction.mli
-rw-r--r-- 6073 proofEngineStructuralRules.ml
-rw-r--r-- 1109 proofEngineStructuralRules.mli
-rw-r--r-- 2400 proofEngineTypes.ml
-rw-r--r-- 2167 proofEngineTypes.mli
-rw-r--r-- 5824 reductionTactics.ml
-rw-r--r-- 1494 reductionTactics.mli
-rw-r--r-- 21749 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 6953 statefulProofEngine.ml
-rw-r--r-- 4174 statefulProofEngine.mli
-rw-r--r-- 9439 tacticChaser.ml
-rw-r--r-- 8222 tacticals.ml
-rw-r--r-- 1900 tacticals.mli
-rw-r--r-- 2919 tactics.ml
-rw-r--r-- 3353 tactics.mli
-rw-r--r-- 4443 variousTactics.ml
-rw-r--r-- 1331 variousTactics.mli