]> matita.cs.unibo.it Git - helm.git/tree - matita/tests/
added splitting engine for .html generated by docbook -> xhtml conversion
[helm.git] / matita / tests /
drwxr-xr-x   ..
-rw-r--r-- 1378 Makefile
-rw-r--r-- 44200 SK.ma
-rw-r--r-- 1327 absurd.ma
-rw-r--r-- 2146 apply.ma
-rw-r--r-- 1586 assumption.ma
drwxr-xr-x - bad_tests
-rw-r--r-- 1740 change.ma
-rw-r--r-- 1354 clear.ma
-rw-r--r-- 1410 clearbody.ma
-rw-r--r-- 2046 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-- 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-- 1406 fix_betareduction.ma
-rw-r--r-- 1445 fold.ma
-rw-r--r-- 1832 generalize.ma
drwxr-xr-x - interactive
-rw-r--r-- 2118 inversion.ma
-rw-r--r-- 1974 inversion2.ma
-rw-r--r-- 1340 letrec.ma
-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
-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-- 1752 unfold.ma