]> matita.cs.unibo.it Git - helm.git/tree - helm/software/matita/tests/
Generation of inductive and inversion principles for mutual
[helm.git] / helm / software / matita / tests /
drwxr-xr-x   ..
drwxr-xr-x - TPTP
-rw-r--r-- 1327 absurd.ma
-rw-r--r-- 2146 apply.ma
-rw-r--r-- 1214 apply2.ma
-rw-r--r-- 1368 applys.ma
-rw-r--r-- 1586 assumption.ma
drwxr-xr-x - bad_tests
-rw-r--r-- 22803 bool.ma
-rw-r--r-- 1740 change.ma
-rw-r--r-- 1354 clear.ma
-rw-r--r-- 1410 clearbody.ma
-rw-r--r-- 2634 coercions.ma
-rw-r--r-- 1440 comments.ma
-rw-r--r-- 1224 constructor.ma
-rw-r--r-- 2303 continuationals.ma
-rw-r--r-- 1403 contradiction.ma
-rw-r--r-- 1247 cut.ma
-rw-r--r-- 6974 decl.ma
-rw-r--r-- 1375 decompose.ma
-rw-r--r-- 1915 demodulation_coq.ma
-rw-r--r-- 1417 demodulation_matita.ma
-rw-r--r-- 1704 discriminate.ma
-rw-r--r-- 2944 elim.ma
-rw-r--r-- 4456 fguidi.ma
-rw-r--r-- 1498 first.ma
-rw-r--r-- 1431 fix_betareduction.ma
-rw-r--r-- 1445 fold.ma
-rw-r--r-- 1832 generalize.ma
-rw-r--r-- 27477 hard_refine.ma
drwxr-xr-x - interactive
-rw-r--r-- 2118 inversion.ma
-rw-r--r-- 1976 inversion2.ma
-rw-r--r-- 1340 letrec.ma
-rw-r--r-- 872 makefile
-rw-r--r-- 1910 match_inference.ma
-rw-r--r-- 4233 metasenv_ordering.ma
-rw-r--r-- 1104 mysql_escaping.ma
-rw-r--r-- 1566 paramodulation.ma
drwxr-xr-x - paramodulation
-rw-r--r-- 1500 record.ma
-rw-r--r-- 1894 replace.ma
-rw-r--r-- 2399 rewrite.ma
-rw-r--r-- 1362 second.ma
-rw-r--r-- 1993 simpl.ma
-rw-r--r-- 1336 test2.ma
-rw-r--r-- 1420 test3.ma
-rw-r--r-- 1477 test4.ma
-rw-r--r-- 1368 third.ma
-rw-r--r-- 1632 tinycals.ma
-rw-r--r-- 1752 unfold.ma