]> matita.cs.unibo.it Git - helm.git/tree - helm/gTopLevel/
Added Decompose tactic
[helm.git] / helm / gTopLevel /
drwxr-xr-x   ..
-rw-r--r-- 34 .cvsignore
-rw-r--r-- 5696 .depend
-rw-r--r-- 3020 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-- 11809 disambiguate.ml
-rw-r--r-- 3134 disambiguate.mli
-rw-r--r-- 23020 doubleTypeInference.ml
-rw-r--r-- 507 doubleTypeInference.mli
-rw-r--r-- 9362 eliminationTactics.ml
-rw-r--r-- 1316 eliminationTactics.mli
-rw-r--r-- 8827 equalityTactics.ml
-rw-r--r-- 1475 equalityTactics.mli
drwxr-xr-x - esempi
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 41956 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 116877 gTopLevel.ml
-rw-r--r-- 1791 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 3746 logicalOperations.ml
-rw-r--r-- 1210 logicalOperations.mli
-rw-r--r-- 19419 mQueryGenerator.ml
-rw-r--r-- 2495 mQueryGenerator.mli
-rw-r--r-- 6247 mQueryLevels.ml
-rw-r--r-- 1831 mQueryLevels.mli
-rw-r--r-- 7167 mQueryLevels2.ml
-rw-r--r-- 1786 mQueryLevels2.mli
-rw-r--r-- 2766 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
-rw-r--r-- 22386 primitiveTactics.ml
-rw-r--r-- 1425 primitiveTactics.mli
-rw-r--r-- 9239 proofEngine.ml
-rw-r--r-- 2778 proofEngine.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-- 22446 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 4297 sequentPp.ml
-rw-r--r-- 1512 sequentPp.mli
-rw-r--r-- 7411 tacticals.ml
-rw-r--r-- 1776 tacticals.mli
drwxr-xr-x - topLevel
-rw-r--r-- 7859 variousTactics.ml
-rw-r--r-- 1229 variousTactics.mli
-rw-r--r-- 2853 xml2Gdome.ml
-rw-r--r-- 1082 xml2Gdome.mli