]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/tactics/
moved tactics from gTopLevel to the new module ocaml/tactics
[helm.git] / helm / ocaml / tactics /
drwxr-xr-x   ..
-rw-r--r-- 39 .cvsignore
-rw-r--r-- 3656 .depend
-rw-r--r-- 744 Makefile
-rw-r--r-- 9362 eliminationTactics.ml
-rw-r--r-- 1316 eliminationTactics.mli
-rw-r--r-- 8827 equalityTactics.ml
-rw-r--r-- 1475 equalityTactics.mli
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 1088 fourier.mli
-rw-r--r-- 42075 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 1791 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 2796 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
-rw-r--r-- 22386 primitiveTactics.ml
-rw-r--r-- 1425 primitiveTactics.mli
-rw-r--r-- 4658 proofEngineHelpers.ml
-rw-r--r-- 1800 proofEngineHelpers.mli
-rw-r--r-- 31098 proofEngineReduction.ml
-rw-r--r-- 1819 proofEngineReduction.mli
-rw-r--r-- 5440 proofEngineStructuralRules.ml
-rw-r--r-- 1109 proofEngineStructuralRules.mli
-rw-r--r-- 1513 proofEngineTypes.ml
-rw-r--r-- 4546 reductionTactics.ml
-rw-r--r-- 1469 reductionTactics.mli
-rw-r--r-- 22450 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 7411 tacticals.ml
-rw-r--r-- 1776 tacticals.mli
-rw-r--r-- 7859 variousTactics.ml
-rw-r--r-- 1229 variousTactics.mli