summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Wed, 06 Oct 1993 10:33:33 +0100 | |

changeset 31 | eb01df4ffe66 |

parent 30 | d49df4181f0d |

child 32 | a8f1cdbbc5b8 |

tctical/dummy_quant_rl: specifies type prop to avoid the type variable
?'a from occurring -- which sometimes caused SELECT_GOAL to fail

--- a/src/Pure/tctical.ML Wed Oct 06 09:58:53 1993 +0100 +++ b/src/Pure/tctical.ML Wed Oct 06 10:33:33 1993 +0100 @@ -395,18 +395,17 @@ The "main goal" of the new state will not be atomic, some tactics may fail! DOES NOT work if tactic affects the main goal other than by instantiation.*) -(* (!!x. ?V) ==> ?V ; used by protect_subgoal.*) +(* (!!x. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*) val dummy_quant_rl = standard (forall_elim_var 0 (assume - (Sign.read_cterm Sign.pure ("!!x. PROP V",propT)))); + (Sign.read_cterm Sign.pure ("!!x::prop. PROP V",propT)))); (* Prevent the subgoal's assumptions from becoming additional subgoals in the new proof state by enclosing them by a universal quantification *) fun protect_subgoal state i = - case Sequence.chop (1, bicompose false (false,dummy_quant_rl,1) i state) - of + case Sequence.chop (1, bicompose false (false,dummy_quant_rl,1) i state) of ([state'],_) => state' - | _ => error"SELECT_GOAL -- impossible error???"; + | _ => error"SELECT_GOAL -- impossible error???"; (*Does the work of SELECT_GOAL. *) fun select (Tactic tf) state i = @@ -416,16 +415,14 @@ in Sequence.flats (Sequence.maps next (tf st0)) end; -(*If i=1 and there is only one subgoal then do nothing!*) fun SELECT_GOAL tac i = Tactic (fn state => case (i, drop(i-1, prems_of state)) of (_,[]) => Sequence.null - | (1,[_]) => tapply(tac,state) + | (1,[_]) => tapply(tac,state) (*If i=1 and only one subgoal do nothing!*) | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal state i) i | (_, _::_) => select tac state i); - (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. Main difference from strip_assums concerns parameters: