Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-05 14:15:43 -0700 (Thu, 05 Jul 2001)
Revision: 3315
Log message:
I have changed the way autoT works.
Now autoT and trivialT share the same auto_resource. When a new tactic is
added to auto_resource, the auto_flag provides information on how to use the
tactic:
- AutoTrivial - use in trivialT; use in autoT before other tactics
- AutoNormal - use in autoT after AutoTrivial tactics
- AutoComplete - use in autoT after AutoTrivial and AutoNormal; use only
if autoT can prove all the genarated subgoals.
I added a few tactics to autoT with AutoComplete flag:
- dT elimination rules (but only when dT will do the thinning)
- JProver with multiplicity 1 (with some assumptions magic); use jAutoT i
to get an autoT version that will run JProver with multiplicity i intead of 1.
I added a flag AutoMustComplete to intro resource flags. This flag takes the
rule to AutoComplete level instead of the usual AutoNormal.
The new autoT no longer does backThruHypT and backThruAssumT (other than through
JProver). I added a new tactic logicAutoT that will do backThruHypT
and backThruAssumT in addition to normal autoT functionality.