]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cc883b4) | patch
- added Ring tactic on reals
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 1 Jul 2002 20:22:39 +0000 (20:22 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 1 Jul 2002 20:22:39 +0000 (20:22 +0000)
commit76cb30ecd0159512548aee0ba7085ab17c6fd5bd
tree06d2b4cfe1f85cf9146b83423dd1ee2ea6985238tree | snapshot
parentcc883b40654c63af2a18d952986277e8e1d59cc9commit | diff
- added Ring tactic on reals
- module splitting
- proofEngine is now almost functional
16 files changed:
helm/gTopLevel/.depend diff | blob | history
helm/gTopLevel/Makefile diff | blob | history
helm/gTopLevel/gTopLevel.ml diff | blob | history
helm/gTopLevel/logicalOperations.ml diff | blob | history
helm/gTopLevel/primitiveTactics.ml [new file with mode: 0644] blob
helm/gTopLevel/primitiveTactics.mli [new file with mode: 0644] blob
helm/gTopLevel/proofEngine.ml diff | blob | history
helm/gTopLevel/proofEngine.mli [new file with mode: 0644] blob
helm/gTopLevel/proofEngineHelpers.ml [new file with mode: 0644] blob
helm/gTopLevel/proofEngineHelpers.mli [new file with mode: 0644] blob
helm/gTopLevel/proofEngineReduction.ml diff | blob | history
helm/gTopLevel/proofEngineStructuralRules.ml [new file with mode: 0644] blob
helm/gTopLevel/proofEngineStructuralRules.mli [new file with mode: 0644] blob
helm/gTopLevel/proofEngineTypes.ml [new file with mode: 0644] blob
helm/gTopLevel/ring.ml [new file with mode: 0644] blob
helm/gTopLevel/ring.mli [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.