]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7adc1d3) | 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)
commit20fcf3075628a59f30db4cc3ce81ea0d0f410d3f
treebbfed381c1bfe7c7a21814a44a912eb7a0dc1111tree | snapshot
parent7adc1d3082ee8d50e236a549a2c341b96becf1fecommit | 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.
helm/software/components/tactics/declarative.ml diff | blob | history
helm/software/components/tactics/tactics.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.