]> matita.cs.unibo.it Git - helm.git/tree - components/tactics/paramodulation/
- transcript: patched to generate aliases instead of inlined variables
[helm.git] / components / tactics / paramodulation /
drwxr-xr-x   ..
-rw-r--r-- 0 .depend
-rw-r--r-- 42 Makefile
-rw-r--r-- 1493 README
-rw-r--r-- 41293 equality.ml
-rw-r--r-- 4918 equality.mli
-rw-r--r-- 4433 equality_indexing.ml
-rw-r--r-- 1546 equality_indexing.mli
-rw-r--r-- 6853 founif.ml
-rw-r--r-- 1626 founif.mli
-rw-r--r-- 39927 indexing.ml
-rw-r--r-- 3282 indexing.mli
-rw-r--r-- 55363 saturation.ml
-rw-r--r-- 2209 saturation.mli
-rw-r--r-- 6921 subst.ml
-rw-r--r-- 1759 subst.mli
-rw-r--r-- 8703 test_indexing.ml
-rw-r--r-- 21858 utils.ml
-rw-r--r-- 2662 utils.mli