]> matita.cs.unibo.it Git - helm.git/commit
A temporary patch to demodulation theorem.
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 19 Sep 2008 06:41:27 +0000 (06:41 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 19 Sep 2008 06:41:27 +0000 (06:41 +0000)
commit04dc7b17e463fa9c75ac91e1df88bf37ed009914
tree066540e5cff6cdeb866cbcc9107a009bed187adf
parent8cc0cbeba5135742b519cc6fb990221e847a12fa
A temporary patch to demodulation theorem.
helm/software/components/tactics/paramodulation/equality.mli
helm/software/components/tactics/paramodulation/indexing.ml
helm/software/components/tactics/paramodulation/indexing.mli
helm/software/components/tactics/paramodulation/saturation.ml