81 (*case*) |
81 (*case*) |
82 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*); |
82 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*); |
83 (*======= end of scanning tacticals, a leaf =======*) |
83 (*======= end of scanning tacticals, a leaf =======*) |
84 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) |
84 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) |
85 = (xxx, (ist |> path_down [L, R]), e); |
85 = (xxx, (ist |> path_down [L, R]), e); |
86 val (a', Program.Tac stac) = interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t; |
86 val (Program.Tac stac, a') = interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t; |
87 |
87 |
88 |
88 |
89 "----------- re-build: fun locate_input_tactic -------------------------------------------------"; |
89 "----------- re-build: fun locate_input_tactic -------------------------------------------------"; |
90 "----------- re-build: fun locate_input_tactic -------------------------------------------------"; |
90 "----------- re-build: fun locate_input_tactic -------------------------------------------------"; |
91 "----------- re-build: fun locate_input_tactic -------------------------------------------------"; |
91 "----------- re-build: fun locate_input_tactic -------------------------------------------------"; |
149 |
149 |
150 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*); |
150 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*); |
151 (*======= end of scanning tacticals, a leaf =======*) |
151 (*======= end of scanning tacticals, a leaf =======*) |
152 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) |
152 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) |
153 = (xxx, (ist |> path_down [R]), e); |
153 = (xxx, (ist |> path_down [R]), e); |
154 val (a', Program.Tac stac) = |
154 val (Program.Tac stac, a') = |
155 (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); |
155 (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); |
156 val Lucin.Ass (m, v', ctxt) = |
156 val Lucin.Ass (m, v', ctxt) = |
157 (*case*) associate pt ctxt (m, stac) (*of*); |
157 (*case*) associate pt ctxt (m, stac) (*of*); |
158 |
158 |
159 Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*); |
159 Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*); |
326 |
326 |
327 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*); |
327 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*); |
328 (*======= end of scanning tacticals, a leaf =======*) |
328 (*======= end of scanning tacticals, a leaf =======*) |
329 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t) |
329 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t) |
330 = (xxx, (ist |> path_down [R]), e); |
330 = (xxx, (ist |> path_down [R]), e); |
331 val (a', Program.Tac stac) = (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); |
331 val (Program.Tac stac, a') = (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); |
332 val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*); |
332 val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*); |
333 val ORundef = (*case*) or (*of*); |
333 val ORundef = (*case*) or (*of*); |
334 val Notappl "norm_equation not applicable" = |
334 val Notappl "norm_equation not applicable" = |
335 (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*); |
335 (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*); |
336 |
336 |