matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Enrico Tassi <enrico.tassi@inria.fr>
	Fri, 29 Sep 2006 12:49:11 +0000 (12:49 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Fri, 29 Sep 2006 12:49:11 +0000 (12:49 +0000)
commit	be87825f491f5eff5f02ee78dd23f34fc0e46e71
tree	391ce864b241222e78dca58bb66ea5743698f972	tree \| snapshot
parent	206c348a9a9900ee3a485a71ac2b10ebd54e6dd8	commit \| diff

new version of auto that is able to prove the irrationality of sqrt(2)

22 files changed:

components/acic_content/.depend		diff \| blob \| history
components/cic/.depend		diff \| blob \| history
components/extlib/.depend		diff \| blob \| history
components/library/.depend		diff \| blob \| history
components/tactics/.depend		diff \| blob \| history
components/tactics/Makefile		diff \| blob \| history
components/tactics/auto.ml		diff \| blob \| history
components/tactics/auto.mli		diff \| blob \| history
components/tactics/autoCache.ml	[new file with mode: 0644]	blob
components/tactics/autoCache.mli	[new file with mode: 0644]	blob
components/tactics/autoTactic.ml		diff \| blob \| history
components/tactics/autoTypes.ml		diff \| blob \| history
components/tactics/autoTypes.mli		diff \| blob \| history
components/tactics/paramodulation/equality.ml		diff \| blob \| history
components/tactics/paramodulation/equality.mli		diff \| blob \| history
components/tactics/paramodulation/equality_retrieval.ml	[new file with mode: 0644]	blob
components/tactics/paramodulation/equality_retrieval.mli	[new file with mode: 0644]	blob
components/tactics/paramodulation/inference.ml		diff \| blob \| history
components/tactics/paramodulation/inference.mli		diff \| blob \| history
components/tactics/paramodulation/saturation.ml		diff \| blob \| history
components/tactics/paramodulation/saturation.mli		diff \| blob \| history
components/tactics/tactics.mli		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.