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	2eaee49a7ff3ed74598a0db84ce4dbc5bca92380
tree	3e73fe6e93af4ca3ba88e6c3a7889e2e247733a3	tree \| snapshot
parent	1f5f06486c55c3db9f2d0fa08e170aab0261943b	commit \| diff

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

22 files changed:

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

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

RSS Atom