]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/tactics/
test branch
[helm.git] / helm / ocaml / tactics /
drwxr-xr-x   ..
-rw-r--r-- 7098 .depend
-rw-r--r-- 771 Makefile
-rw-r--r-- 11736 autoTactic.ml
-rw-r--r-- 1358 autoTactic.mli
-rw-r--r-- 11542 continuationals.ml
-rw-r--r-- 3629 continuationals.mli
-rw-r--r-- 28488 discriminationTactics.ml
-rw-r--r-- 1220 discriminationTactics.mli
drwxr-xr-x - doc
-rw-r--r-- 9427 eliminationTactics.ml
-rw-r--r-- 1328 eliminationTactics.mli
-rw-r--r-- 14122 equalityTactics.ml
-rw-r--r-- 1549 equalityTactics.mli
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 1088 fourier.mli
-rw-r--r-- 43538 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 5855 fwdSimplTactic.ml
-rw-r--r-- 1294 fwdSimplTactic.mli
-rw-r--r-- 20075 hashtbl_equiv.ml
-rw-r--r-- 1690 hashtbl_equiv.mli
-rw-r--r-- 2997 history.ml
-rw-r--r-- 1147 history.mli
-rw-r--r-- 1977 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 9351 inversion.ml
-rw-r--r-- 1050 inversion.mli
-rw-r--r-- 12851 metadataQuery.ml
-rw-r--r-- 1983 metadataQuery.mli
-rw-r--r-- 3124 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
-rw-r--r-- 21748 primitiveTactics.ml
-rw-r--r-- 2161 primitiveTactics.mli
-rw-r--r-- 27073 proofEngineHelpers.ml
-rw-r--r-- 4893 proofEngineHelpers.mli
-rw-r--r-- 36036 proofEngineReduction.ml
-rw-r--r-- 1966 proofEngineReduction.mli
-rw-r--r-- 6726 proofEngineStructuralRules.ml
-rw-r--r-- 1406 proofEngineStructuralRules.mli
-rw-r--r-- 3073 proofEngineTypes.ml
-rw-r--r-- 2613 proofEngineTypes.mli
-rw-r--r-- 8501 reductionTactics.ml
-rw-r--r-- 1754 reductionTactics.mli
-rw-r--r-- 22670 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 6965 statefulProofEngine.ml
-rw-r--r-- 4174 statefulProofEngine.mli
-rw-r--r-- 9335 tacticChaser.ml
-rw-r--r-- 12080 tacticals.ml
-rw-r--r-- 2915 tacticals.mli
-rw-r--r-- 3023 tactics.ml
-rw-r--r-- 3828 tactics.mli
-rw-r--r-- 6806 variousTactics.ml
-rw-r--r-- 1228 variousTactics.mli