131 | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); |
131 | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); |
132 Seq.make(fn()=> seqcell)); |
132 Seq.make(fn()=> seqcell)); |
133 |
133 |
134 (*Makes a rule by applying a tactic to an existing rule*) |
134 (*Makes a rule by applying a tactic to an existing rule*) |
135 fun rule_by_tactic tac rl = |
135 fun rule_by_tactic tac rl = |
136 let val (st, thaw) = freeze_thaw_robust (zero_var_indexes rl) |
136 let |
137 in case Seq.pull (tac st) of |
137 val ctxt = Variable.thm_context rl; |
138 NONE => raise THM("rule_by_tactic", 0, [rl]) |
138 val ([st], ctxt') = Variable.import true [rl] ctxt; |
139 | SOME(st',_) => Thm.varifyT (thaw 0 st') |
139 in |
|
140 (case Seq.pull (tac st) of |
|
141 NONE => raise THM ("rule_by_tactic", 0, [rl]) |
|
142 | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st')) |
140 end; |
143 end; |
|
144 |
141 |
145 |
142 (*** Basic tactics ***) |
146 (*** Basic tactics ***) |
143 |
147 |
144 (*** The following fail if the goal number is out of range: |
148 (*** The following fail if the goal number is out of range: |
145 thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) |
149 thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) |