]> matita.cs.unibo.it Git - helm.git/tree - helm/gTopLevel/
Added new tactics: Exists, Split, Assumption, Absurd, Generalize (doesn't work)
[helm.git] / helm / gTopLevel /
drwxr-xr-x   ..
-rw-r--r-- 34 .cvsignore
-rw-r--r-- 3829 .depend
-rw-r--r-- 2611 Makefile
-rw-r--r-- 5074 TATTICHE
-rw-r--r-- 16510 cic2Xml.ml
-rw-r--r-- 1549 cic2Xml.mli
-rw-r--r-- 16333 cic2acic.ml
-rw-r--r-- 2362 cic2acic.mli
-rw-r--r-- 23020 doubleTypeInference.ml
-rw-r--r-- 507 doubleTypeInference.mli
drwxr-xr-x - esempi
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 41837 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 91509 gTopLevel.ml
-rw-r--r-- 3746 logicalOperations.ml
-rw-r--r-- 1210 logicalOperations.mli
-rw-r--r-- 5572 mQueryGenerator.ml
-rw-r--r-- 2190 mQueryGenerator.mli
-rw-r--r-- 6890 mQueryLevels.ml
-rw-r--r-- 2115 mQueryLevels.mli
-rw-r--r-- 6953 mQueryLevels2.ml
-rw-r--r-- 2041 mQueryLevels2.mli
-rw-r--r-- 22418 primitiveTactics.ml
-rw-r--r-- 1441 primitiveTactics.mli
-rw-r--r-- 8904 proofEngine.ml
-rw-r--r-- 2616 proofEngine.mli
-rw-r--r-- 4346 proofEngineHelpers.ml
-rw-r--r-- 1763 proofEngineHelpers.mli
-rw-r--r-- 29416 proofEngineReduction.ml
-rw-r--r-- 1673 proofEngineReduction.mli
-rw-r--r-- 5440 proofEngineStructuralRules.ml
-rw-r--r-- 1109 proofEngineStructuralRules.mli
-rw-r--r-- 1513 proofEngineTypes.ml
-rw-r--r-- 4542 reductionTactics.ml
-rw-r--r-- 1417 reductionTactics.mli
-rw-r--r-- 22418 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 4297 sequentPp.ml
-rw-r--r-- 1512 sequentPp.mli
-rw-r--r-- 7406 tacticals.ml
-rw-r--r-- 1776 tacticals.mli
drwxr-xr-x - topLevel
-rw-r--r-- 18033 variousTactics.ml
-rw-r--r-- 2097 variousTactics.mli
-rw-r--r-- 2853 xml2Gdome.ml
-rw-r--r-- 1082 xml2Gdome.mli