84 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*) |
84 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*) |
85 assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e ; |
85 assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e ; |
86 (*======= end of scanning tacticals, a leaf =======*) |
86 (*======= end of scanning tacticals, a leaf =======*) |
87 "~~~~~ fun assy, args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t) = |
87 "~~~~~ fun assy, args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t) = |
88 (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e); |
88 (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e); |
89 val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*); |
89 val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr (E, (a, v)) t (*of*); |
90 |
90 |
91 (*val Ass (m,v') = in isabisacREP*) |
91 (*val Ass (m,v') = in isabisacREP*) |
92 (*val NotAss = in isabisac*) |
92 (*val NotAss = in isabisac*) |
93 (*case*) associate pt ctxt (m, stac) (*of*); |
93 (*case*) associate pt ctxt (m, stac) (*of*); |
94 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))), |
94 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))), |
231 = (thy, ptp, E, (up @ [Celem.R, Celem.D]), body, a, v); |
231 = (thy, ptp, E, (up @ [Celem.R, Celem.D]), body, a, v); |
232 |
232 |
233 (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e a v (*of*); |
233 (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e a v (*of*); |
234 "~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v) |
234 "~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v) |
235 = (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v); |
235 = (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v); |
236 val (a', STac stac) = (*case*) Lucin.handle_leaf "next " th sr E a v t (*of*); |
236 val (a', STac stac) = (*case*) Lucin.handle_leaf "next " th sr (E, (a, v)) t (*of*); |
237 |
237 |
238 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy th) stac; |
238 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy th) stac; |
239 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags')) |
239 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags')) |
240 = (pt, (Celem.assoc_thy th), stac); |
240 = (pt, (Celem.assoc_thy th), stac); |
241 val (dI, pI, mI) = Prog_Tac.dest_spec spec' |
241 val (dI, pI, mI) = Prog_Tac.dest_spec spec' |