]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c6d5b3c) | patch
The declarative rewriting step now tries auto timeout=3 before
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Apr 2007 15:33:27 +0000 (15:33 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Apr 2007 15:33:27 +0000 (15:33 +0000)
commit38548f400ba9acfa45d70ca814080ca80a2f9aac
tree109e93d2c97e47035ab8ca58bb14c3cdb94e8d2ctree | snapshot
parentc6d5b3c8a2e808fd697cd1560878577431da588bcommit | diff
The declarative rewriting step now tries auto timeout=3 before
auto paramodulation timeout=3. This seems to work better then just
auto paramodulation alone when the user tries to help the system.
This because paramodulation is more confused than helped.
components/tactics/declarative.ml diff | blob | history
components/tactics/tactics.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.