]> matita.cs.unibo.it Git - helm.git/commit
new version of auto that is able to prove the irrationality of sqrt(2)
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 29 Sep 2006 12:49:11 +0000 (12:49 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 29 Sep 2006 12:49:11 +0000 (12:49 +0000)
commit2eaee49a7ff3ed74598a0db84ce4dbc5bca92380
tree3e73fe6e93af4ca3ba88e6c3a7889e2e247733a3
parent1f5f06486c55c3db9f2d0fa08e170aab0261943b
new version of auto that is able to prove the irrationality of sqrt(2)
22 files changed:
helm/software/components/acic_content/.depend
helm/software/components/cic/.depend
helm/software/components/extlib/.depend
helm/software/components/library/.depend
helm/software/components/tactics/.depend
helm/software/components/tactics/Makefile
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/autoCache.ml [new file with mode: 0644]
helm/software/components/tactics/autoCache.mli [new file with mode: 0644]
helm/software/components/tactics/autoTactic.ml
helm/software/components/tactics/autoTypes.ml
helm/software/components/tactics/autoTypes.mli
helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/tactics/paramodulation/equality.mli
helm/software/components/tactics/paramodulation/equality_retrieval.ml [new file with mode: 0644]
helm/software/components/tactics/paramodulation/equality_retrieval.mli [new file with mode: 0644]
helm/software/components/tactics/paramodulation/inference.ml
helm/software/components/tactics/paramodulation/inference.mli
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/paramodulation/saturation.mli
helm/software/components/tactics/tactics.mli