243 (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Complete |
243 (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Complete |
244 val pt = update_branch pt p TransitiveB |
244 val pt = update_branch pt p TransitiveB |
245 in |
245 in |
246 ((p, Res), c, FormKF (UnparseC.term f'), pt) |
246 ((p, Res), c, FormKF (UnparseC.term f'), pt) |
247 end |
247 end |
248 | generate1 (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, _)) (is, ctxt) (pt, (p, _)) = |
|
249 let |
|
250 val (pt, _) = cappend_form pt p (is, ctxt) f |
|
251 val pt = update_branch pt p TransitiveB |
|
252 val is = init_istate (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs, Rule_Set.id rls)) f |
|
253 val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt) |
|
254 val pos' = ((lev_on o lev_dn) p, Frm) |
|
255 in |
|
256 generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*) |
|
257 end |
|
258 | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) = |
248 | generate1 (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) = |
259 let |
249 let |
260 val (pt, c) = cappend_atomic pt p (is, ctxt) f |
250 val (pt, c) = cappend_atomic pt p (is, ctxt) f |
261 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Complete |
251 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Complete |
262 val pt = update_branch pt p TransitiveB |
252 val pt = update_branch pt p TransitiveB |
263 in |
253 in |
264 ((p, Res), c, FormKF (UnparseC.term f'), pt) |
254 ((p, Res), c, FormKF (UnparseC.term f'), pt) |
265 end |
|
266 | generate1 (Tactic.Detail_Set' (_, _, rls, f, _)) (is, ctxt) (pt, (p, _)) = |
|
267 let |
|
268 val (pt, _) = cappend_form pt p (is, ctxt) f |
|
269 val pt = update_branch pt p TransitiveB |
|
270 val is = init_istate (Tactic.Rewrite_Set (Rule_Set.id rls)) f |
|
271 val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt) |
|
272 val pos' = ((lev_on o lev_dn) p, Frm) |
|
273 in |
|
274 generate1 tac_ (is, ctxt) (pt, pos') (*implicit Take*) |
|
275 end |
255 end |
276 | generate1 (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) = |
256 | generate1 (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) = |
277 let |
257 let |
278 val (pt, c) = append_result pt p l (scval, []) Complete |
258 val (pt, c) = append_result pt p l (scval, []) Complete |
279 in |
259 in |