1.1 --- a/test/Tools/isac/Test_Some.thy Wed May 27 16:20:06 2020 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Thu May 28 12:52:25 2020 +0200
1.3 @@ -56,7 +56,7 @@
1.4 ML \<open>
1.5 "~~~~~ fun xxx , args:"; val () = ();
1.6 "~~~~~ and xxx , args:"; val () = ();
1.7 -"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
1.8 +"~~~~~ fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
1.9 (*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*);
1.10 "xx"
1.11 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
1.12 @@ -92,8 +92,20 @@
1.13 section \<open>===================================================================================\<close>
1.14 ML \<open>
1.15 \<close> ML \<open>
1.16 -fun on_calc_end ([], Res) = true
1.17 - | on_calc_end _ = false;
1.18 +\<close> ML \<open>
1.19 +\<close> ML \<open>
1.20 +\<close>
1.21 +
1.22 +section \<open>===================================================================================\<close>
1.23 +ML \<open>
1.24 +\<close> ML \<open>
1.25 +\<close> ML \<open>
1.26 +\<close> ML \<open>
1.27 +\<close>
1.28 +
1.29 +section \<open>===================================================================================\<close>
1.30 +ML \<open>
1.31 +\<close> ML \<open>
1.32 \<close> ML \<open>
1.33 \<close> ML \<open>
1.34 \<close>
1.35 @@ -173,7 +185,7 @@
1.36 (*+*)val (_, ["Biegelinien"], _) = spec;
1.37 (*\------------------- initial check for whole me ------------------------------------------/*)
1.38 \<close> ML \<open>
1.39 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.40 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.41 \<close> ML \<open>
1.42 (*/------------------- begin step into Step.by_tactic --------------------------------------\*)
1.43 val (pt'''''_', p'''''_') =
1.44 @@ -196,28 +208,30 @@
1.45 (*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";
1.46 \<close> ML \<open>
1.47 \<close> ML \<open>
1.48 -(*\------------------- initial check forStep.by_tactic -------------------------------------/*)
1.49 +(*\------------------- initial check for Step.by_tactic ------------------------------------/*)
1.50 (*\------------------- step into Step.by_tactic --------------------------------------------/*)
1.51 +
1.52 +\<close> ML \<open>
1.53 (*/------------------- step into Step.do_next ----------------------------------------------\*)
1.54 (**)val ("dummy", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) = (**)
1.55 (*case*)
1.56 Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);
1.57 \<close> ML \<open>
1.58 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
1.59 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
1.60 (p'''''_', ((pt'''''_', Pos.e_pos'), []));
1.61 \<close> ML \<open>
1.62 -(*NEW*)(*if*) Pos.on_calc_end ip (*else*);
1.63 +(*.NEW*)(*if*) Pos.on_calc_end ip (*else*);
1.64 \<close> ML \<open>
1.65 -(*NEW*) val (_, probl_id, _) = Calc.references (pt, p);
1.66 +(*.NEW*) val (_, probl_id, _) = Calc.references (pt, p);
1.67 \<close> ML \<open>
1.68 (*-"-*) val _ = (*case*) tacis (*of*);
1.69 \<close> ML \<open>
1.70 -(*NEW*) (*if*) probl_id = Problem.id_empty (*else*);
1.71 +(*.NEW*) (*if*) probl_id = Problem.id_empty (*else*);
1.72 \<close> ML \<open>
1.73 (**)val ("dummy", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) = (**)
1.74 -(*NEW*) switch_specify_solve p_ (pt, ip)
1.75 +(*.NEW*) switch_specify_solve p_ (pt, ip)
1.76 \<close> ML \<open>
1.77 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.78 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.79 \<close> ML \<open>
1.80 (*if*) Pos.on_specification ([], state_pos) (*then*);
1.81 \<close> ML \<open>
1.82 @@ -247,7 +261,7 @@
1.83 "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]"
1.84 (*\------------------- check for entry to specify_do_next ----------------------------------/*)
1.85 \<close> ML \<open>
1.86 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
1.87 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
1.88 \<close> ML \<open>
1.89 \<close> ML \<open>
1.90 (**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)
1.91 @@ -255,10 +269,10 @@
1.92 \<close> ML \<open>
1.93 "~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = (ptp);
1.94 \<close> ML \<open>
1.95 -(*NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _),
1.96 -(*NEW*) probl = pbl, spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
1.97 +(*.NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _),
1.98 +(*.NEW*) probl = pbl, spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
1.99 \<close> ML \<open>
1.100 -(*NEW*)(*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
1.101 +(*.NEW*)(*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
1.102 \<close> ML \<open>
1.103 val cpI = if pI = Problem.id_empty then pI' else pI;
1.104 val cmI = if mI = Method.id_empty then mI' else mI;
1.105 @@ -285,7 +299,7 @@
1.106 (*case*) item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
1.107 \<close> ML \<open>
1.108 (*redes: here we have all m_field ------------------vvvv *)
1.109 -"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms) =
1.110 +"~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =
1.111 ((ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
1.112 \<close> ML \<open>
1.113 (*OLD*)fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v (**)andalso (#3 ori) <> "#undef"(**)
1.114 @@ -338,13 +352,13 @@
1.115
1.116 SOME
1.117 (I_Model.geti_ct thy ori (hd icl)) (*return from item_to_add*);
1.118 -"~~~~~ fun geti_ct , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
1.119 +"~~~~~ ~~ fun geti_ct , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
1.120 \<close> ML \<open>
1.121 val rrrrr =
1.122 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join)
1.123 (d, subtract op = (ts_in itm_) ts)) (*return from geti_ct*);
1.124 \<close> ML \<open>
1.125 -"~~~~~ from fun geti_ct \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
1.126 +"~~~~~ ~~ from fun geti_ct \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
1.127 (SOME rrrrr);
1.128 \<close> ML \<open>
1.129 ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
1.130 @@ -368,11 +382,11 @@
1.131 (*//ERROR by_tactic_input' Met: uncovered case of#undef*)
1.132 Specify.by_tactic_input' "#Given" ct ptp (*return from by_tactic_input*);
1.133 \<close> ML \<open>
1.134 -"~~~~~ fun by_tactic_input' , args:"; val (sel, ct, (ptp as (pt, (p, Pos.Met)))) = ("#Given", ct, ptp);
1.135 +"~~~~~ ~ fun by_tactic_input' , args:"; val (sel, ct, (ptp as (pt, (p, Pos.Met)))) = ("#Given", ct, ptp);
1.136 \<close> ML \<open>
1.137 -(*+*)ct = "FunktionsVariable x"
1.138 +(*+*)ct = "FunktionsVariable x";
1.139 \<close> ML \<open>
1.140 -(*NEW*)val sel = "#undef"; (* m_field may change from root- to sub-Model_Pattern *)
1.141 +(*///NEW* )val sel = "#undef"; (**) m_field may change from root- to sub-Model_Pattern *)
1.142 val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of
1.143 Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
1.144 (oris, dI', mI', dI, mI, met, ctxt)
1.145 @@ -380,49 +394,18 @@
1.146 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
1.147 val cmI = if mI = Method.id_empty then mI' else mI;
1.148 \<close> ML \<open>
1.149 -(*/------------------- build new fun for Model_Pattern -------------------------------------\*)
1.150 -val descriptor = @{term "FunktionsVariable"}
1.151 -\<close> ML \<open>
1.152 -fun get_field descriptor m_patt =
1.153 - (filter ((curry (fn (desc, (_, (desc', _))) => desc = desc')) descriptor) m_patt
1.154 - |> the_single
1.155 - |> (fn (a, _) => SOME a))
1.156 - handle List.Empty => NONE
1.157 -(*\------------------- build new fun for Model_Pattern ------------------------------------/*)
1.158 -(*/------------------- build new fun for I_Model -------------------------------------\*)
1.159 -\<close> ML \<open>
1.160 -fun check_single ctxt _ o_model i_model m_patt str =
1.161 - case TermC.parseNEW ctxt str of
1.162 - NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")
1.163 - | SOME (t as (descriptor $ _)) =>
1.164 -(*NEW*) (case get_field descriptor m_patt of
1.165 -(*NEW*) NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
1.166 - UnparseC.term_in_ctxt ctxt descriptor ^ "\"")
1.167 -(*NEW*) | SOME m_field =>
1.168 -(*NEW*)
1.169 - case O_Model.is_known ctxt m_field o_model t of
1.170 - ("", ori', all) =>
1.171 - (case is_notyet_input ctxt i_model all ori' m_patt of
1.172 - ("", itm) => Add itm
1.173 - | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
1.174 - | (msg, _, _) => Err ("ERROR I_Model.check_single: is_known: " ^ msg))
1.175 -(*NEW*)| SOME t => Err ("ERROR I_Model.check_single: impossible for input \"" ^
1.176 -(*NEW*) UnparseC.term_in_ctxt ctxt t ^ "\"");
1.177 -(*\------------------- build new fun for I_Model ------------------------------------/*)
1.178 -\<close> ML \<open>
1.179 -(*--- should be -------"#Given"-vvv *)
1.180 -val Add (5, [1], true, "#undef", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("v", _), [Free ("x", _)]))) =
1.181 +val Add (5, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("v", _), [Free ("x", _)]))) =
1.182 (*case*)
1.183 I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct (*of*);
1.184 \<close> ML \<open>
1.185 -"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
1.186 +"~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
1.187 (ctxt, sel, oris, met, ((#ppc o Method.from_store) cmI), ct);
1.188 \<close> ML \<open>
1.189 (*OLD* )| SOME t =>
1.190 -( *NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*);
1.191 +( *.NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*);
1.192 \<close> ML \<open>
1.193 -(*NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
1.194 -(*NEW*)
1.195 +(*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
1.196 +(*.NEW*)
1.197 \<close> ML \<open>
1.198 (*+*)O_Model.to_string o_model = "[\n" ^
1.199 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
1.200 @@ -434,11 +417,11 @@
1.201 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
1.202 \<close> ML \<open>
1.203 (**)
1.204 -(*("[x] not for #Given", (0, [], "", Const ("empty", "??.'a"), [Const ("empty", "??.'a")]), [])*)
1.205 +val ("", (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), [Free ("x", _)]) =
1.206 (*case*)
1.207 O_Model.is_known ctxt m_field o_model t (*of*);
1.208 \<close> ML \<open>
1.209 -"~~~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
1.210 +"~~~~~ ~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
1.211 \<close> ML \<open>
1.212 val ots = (LibraryC.distinct o flat o (map #5)) ori
1.213 val oids = ((map (fst o dest_Free)) o LibraryC.distinct o flat o (map TermC.vars)) ots
1.214 @@ -453,7 +436,7 @@
1.215 \<close> ML \<open>
1.216 seek_oridts ctxt sel (d, ts) ori
1.217 \<close> ML \<open>
1.218 -"~~~~~ fun seek_oridts , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
1.219 +"~~~~~ ~~~~ fun seek_oridts , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
1.220 (ctxt, sel, (d, ts), ori);
1.221 \<close> ML \<open>
1.222 (*+*)val Add_Given "FunktionsVariable x" = tac
1.223 @@ -475,7 +458,8 @@
1.224 \<close> ML \<open>
1.225 (*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
1.226 \<close> ML \<open>
1.227 -(*+*)m_field' = "#undef"; (*MUST BE *)
1.228 +(*+*)val (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]) =
1.229 + (id, vat, m_field', descript', vals')
1.230 \<close> ML \<open>
1.231 \<close> ML \<open>
1.232 (*-------------------- stop step into whole me ----------------------------------------------*)
1.233 @@ -518,11 +502,11 @@
1.234 (*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
1.235 (*+*)(* by ^^^^^^^^^^^^ "id_fun" and "id_abl" must be requested: PUT THEM INTO O_Model*)
1.236
1.237 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.238 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.239
1.240 val ("ok", ([], [], (_, _))) = (*case*)
1.241 Step.by_tactic tac (pt, p) (*of*);
1.242 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.243 +"~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.244 val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);
1.245 (*if*) Tactic.for_specify' tac' (*then*);
1.246
1.247 @@ -544,7 +528,7 @@
1.248 then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY Method";
1.249 (*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
1.250 \<close> ML \<open>
1.251 -"~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
1.252 +"~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
1.253 (tac', ptp);
1.254 (*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
1.255 (*NEW*) ...} =Calc.specify_data (pt, pos);
1.256 @@ -589,19 +573,9 @@
1.257 (*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
1.258 \<close> ML \<open>
1.259 O_Model.complete_for_from m_patt o_model (root_model, ctxt);
1.260 -"~~~~~ fun complete_for_from , args:"; val (m_patt, root_model, (o_model, ctxt)) =
1.261 +"~~~~ fun complete_for_from , args:"; val (m_patt, root_model, (o_model, ctxt)) =
1.262 (m_patt, root_model, (o_model, ctxt));
1.263 \<close> ML \<open>
1.264 -(*/------------------- build new fun complete_for_from -------------------------------------\*)
1.265 -(*/----- values for building -------------\* )
1.266 -val d1 $ v1 = @{term "errorBound eee_val"};
1.267 -val d2 $ v2 = @{term "boundVariable bbb"};
1.268 -val root_model = root_model @ [(11, [1], "#undef", d1, [v1]), (22, [1], "#undef", d2, [v2])];
1.269 -
1.270 -val d $ v = @{term "errorBound eee_var"};
1.271 -val m_patt = m_patt @ [("#Relate", (d, v))];
1.272 -( *\----- values for building -------------/*)
1.273 -\<close> ML \<open>
1.274 val missing = m_patt |> filter_out
1.275 (fn (_, (descriptor, _)) => (Library.member op = (map #4 o_model) descriptor))
1.276 \<close> ML \<open>
1.277 @@ -616,8 +590,7 @@
1.278 |> add_id
1.279 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
1.280 ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from complete_for_from*);
1.281 -(*\------------------- build new fun complete_for_from -------------------------------------/*)
1.282 -"~~~~~ from fun complete_for_from \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
1.283 +"~~~~ from fun complete_for_from \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
1.284 ((o_model @ add)
1.285 |> map (fn (_, b, c, d, e) => (b, c, d, e))
1.286 |> add_id
1.287 @@ -652,7 +625,7 @@
1.288 (*+*)pos = ([1], Met);
1.289
1.290 ("ok", ([], [], (pt, pos))) (*return from Step_Specify.by_tactic*);
1.291 -"~~~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
1.292 +"~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
1.293 ("ok", ([], [], (pt, pos)));
1.294 (* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
1.295 (* SHOULD BE ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
1.296 @@ -661,7 +634,7 @@
1.297 (*("helpless", ([], [], ..*)
1.298 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1.299 \<close> ML \<open>
1.300 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
1.301 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
1.302 (*NEW*)(*if*) on_calc_end ip (*else*);
1.303 (*NEW*) val (_, probl_id, _) = Calc.references (pt, p);
1.304 (*-"-*) val _ = (*case*) tacis (*of*);
1.305 @@ -672,12 +645,12 @@
1.306 (*NEW*)val ("dummy", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
1.307 (*NEW*) switch_specify_solve p_ (pt, ip);
1.308 \<close> ML \<open>
1.309 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.310 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.311 (*if*) Pos.on_specification ([], state_pos) (*then*);
1.312
1.313 val ("dummy", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
1.314 specify_do_next (pt, input_pos);
1.315 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
1.316 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
1.317
1.318 val (_, (p_', tac)) =
1.319 Specify.find_next_step ptp;
1.320 @@ -737,7 +710,7 @@
1.321 "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
1.322 "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
1.323
1.324 -"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
1.325 +"~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
1.326
1.327 \<close> ML \<open>
1.328 Specify.by_tactic_input' "#Given" ct ptp;
1.329 @@ -772,7 +745,7 @@
1.330 (*\------------------- check for entry to check_single -------------------------------------/*)
1.331 \<close> ML \<open>
1.332
1.333 -"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
1.334 +"~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
1.335 (ctxt, sel, oris, met, ((#ppc o Method.from_store) cmI), ct);
1.336 val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);
1.337
1.338 @@ -781,7 +754,7 @@
1.339 (*("seek_oridts: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)
1.340 (*case*)
1.341 is_known ctxt m_field o_model t (*of*);
1.342 -"~~~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
1.343 +"~~~~~ ~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
1.344 val ots = (LibraryC.distinct o flat o (map #5)) ori
1.345 val oids = ((map (fst o dest_Free)) o LibraryC.distinct o flat o (map TermC.vars)) ots
1.346 val (d, ts) = Input_Descript.split t
1.347 @@ -791,7 +764,7 @@
1.348 (*if*) not (subset op = (map typeless ts, map typeless ots)) (*else*);
1.349
1.350 (*case*) O_Model.seek_orits ctxt sel ts ori (*of*);
1.351 -"~~~~~ fun seek_orits , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
1.352 +"~~~~~ ~~~ fun seek_orits , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
1.353
1.354 (*+/---------------- bypass recursion of seek_orits ----------------\*)
1.355 (*+*)O_Model.to_string oris = "[\n" ^