1.1 --- a/src/Tools/isac/BridgeJEdit/template.sml Wed Sep 20 08:27:21 2023 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/template.sml Wed Sep 20 11:30:50 2023 +0200
1.3 @@ -76,14 +76,14 @@
1.4
1.5 (** create output format **)
1.6
1.7 -fun item_to_out ctxt (_, _, _, _, (I_Model.Cor_TEST (dsc_ts, _), _)) =
1.8 +fun item_to_out ctxt (_, _, _, _, (I_Model.Cor_TEST dsc_ts, _)) =
1.9 (dsc_ts |> Term.list_comb |> UnparseC.term ctxt, Correct)
1.10 | item_to_out _ (_, _, _, _, (I_Model.Syn_TEST (term_as_string), _)) =
1.11 (term_as_string, Incomplete)
1.12
1.13 - | item_to_out ctxt (_, _, _, _, (I_Model.Inc_TEST ((dsc, []), _), _)) =
1.14 + | item_to_out ctxt (_, _, _, _, (I_Model.Inc_TEST (dsc, []), _)) =
1.15 (UnparseC.term ctxt dsc ^ " " ^ Model_Pattern.empty_for dsc, Incomplete)
1.16 - | item_to_out ctxt (_, _, _, _, (I_Model.Inc_TEST (dsc_ts, _), _)) =
1.17 + | item_to_out ctxt (_, _, _, _, (I_Model.Inc_TEST (dsc_ts), _)) =
1.18 (dsc_ts |> Term.list_comb |> UnparseC.term ctxt, Incomplete)
1.19
1.20 | item_to_out ctxt (_, _, _, _, (I_Model.Sup_TEST dsc_ts, _)) =
2.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Wed Sep 20 08:27:21 2023 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Wed Sep 20 11:30:50 2023 +0200
2.3 @@ -38,11 +38,11 @@
2.4 fun extract (_, _, _, _, itm_) = itm_
2.5 in map (xml_of_itm_ o extract) itms end
2.6 (*T_TEST*)
2.7 -fun xml_of_itm_TEST (I_Model.Cor_TEST (dts, _)) =
2.8 +fun xml_of_itm_TEST (I_Model.Cor_TEST dts) =
2.9 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])
2.10 | xml_of_itm_TEST (I_Model.Syn_TEST c) =
2.11 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
2.12 - | xml_of_itm_TEST (I_Model.Inc_TEST (dts, _)) =
2.13 + | xml_of_itm_TEST (I_Model.Inc_TEST dts) =
2.14 XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])
2.15 | xml_of_itm_TEST (I_Model.Sup_TEST dts) =
2.16 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])
3.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Sep 20 08:27:21 2023 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Sep 20 11:30:50 2023 +0200
3.3 @@ -103,11 +103,11 @@
3.4 fun extract (_, _, _, _, itm_) = itm_
3.5 in map (xml_of_itm_ o extract) itms end
3.6 (*T_TEST*)
3.7 -fun xml_of_itm_TEST (I_Model.Cor_TEST (dts, _)) =
3.8 +fun xml_of_itm_TEST (I_Model.Cor_TEST dts) =
3.9 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])
3.10 | xml_of_itm_TEST (I_Model.Syn_TEST c) =
3.11 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
3.12 - | xml_of_itm_TEST (I_Model.Inc_TEST (dts, _)) =
3.13 + | xml_of_itm_TEST (I_Model.Inc_TEST dts) =
3.14 XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])
3.15 | xml_of_itm_TEST (I_Model.Sup_TEST dts) =
3.16 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])
4.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Wed Sep 20 08:27:21 2023 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Wed Sep 20 11:30:50 2023 +0200
4.3 @@ -38,9 +38,9 @@
4.4 | Mis of (term * term)
4.5 | Par of TermC.as_string
4.6 datatype i_model_feedback_TEST =
4.7 - Cor_TEST of (descriptor * (term list)) * (term * (term list))
4.8 + Cor_TEST of (descriptor * (term list))
4.9 | Syn_TEST of TermC.as_string
4.10 - | Inc_TEST of (descriptor * (term list)) * (term * (term list))
4.11 + | Inc_TEST of (descriptor * (term list))
4.12 | Sup_TEST of (descriptor * (term list))
4.13 val feedback_empty_TEST: i_model_feedback_TEST
4.14
4.15 @@ -100,13 +100,12 @@
4.16 *)
4.17 datatype i_model_feedback_TEST =
4.18 Cor_TEST of (descriptor * (* correct input: descriptor, see Input_Descript.thy *)
4.19 - (values)) * (* set of values for list-types: for decdiing
4.20 + (values)) (* set of values for list-types: for decding
4.21 Inc the values packed out from the list;
4.22 They are packed back to an isalist for envs *)
4.23 - (term * (term list)) (* will be eliminated in i_model_feedback_TEST *)
4.24 | Syn_TEST of TermC.as_string (* syntax error kept for P_Model.switch_pbl_met *)
4.25 -| Inc_TEST of (descriptor * values) * (term * (term list)) (* see Cor *)
4.26 -| Sup_TEST of (descriptor * values)(* superfluous; input not found in O_Model.T *)
4.27 +| Inc_TEST of (descriptor * values) (* see Cor *)
4.28 +| Sup_TEST of (descriptor * values) (* superfluous; input not found in O_Model.T *)
4.29 val feedback_empty_TEST = Syn_TEST "i_model_empty"
4.30
4.31
5.1 --- a/src/Tools/isac/Specify/i-model.sml Wed Sep 20 08:27:21 2023 +0200
5.2 +++ b/src/Tools/isac/Specify/i-model.sml Wed Sep 20 11:30:50 2023 +0200
5.3 @@ -131,10 +131,10 @@
5.4 type env = Env.T
5.5
5.6
5.7 -fun feedback_OLD_to_TEST (Cor ((d, ts), penv)) = (Model_Def.Cor_TEST ((d, ts), penv))
5.8 +fun feedback_OLD_to_TEST (Cor ((d, ts), penv)) = (Model_Def.Cor_TEST (d, ts))
5.9 | feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)
5.10 | feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)
5.11 - | feedback_OLD_to_TEST (Inc ((d, ts), penv)) = (Model_Def.Inc_TEST ((d, ts), penv))
5.12 + | feedback_OLD_to_TEST (Inc ((d, ts), penv)) = (Model_Def.Inc_TEST (d, ts))
5.13 | feedback_OLD_to_TEST (Sup (d, ts)) = (Model_Def.Sup_TEST (d, ts))
5.14 | feedback_OLD_to_TEST (Mis (d, pid)) = Model_Def.Syn_TEST ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
5.15 (UnparseC.term (ContextC.for_ERROR ()) pid))
5.16 @@ -142,9 +142,9 @@
5.17 fun OLD_to_TEST i_old =
5.18 map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_TEST e, Position.none))) i_old
5.19
5.20 -fun feedback_TEST_to_OLD (Model_Def.Cor_TEST ((d, ts), penv)) = (Cor ((d, ts), penv))
5.21 +fun feedback_TEST_to_OLD (Model_Def.Cor_TEST (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
5.22 | feedback_TEST_to_OLD (Model_Def.Syn_TEST c) = (Syn c)
5.23 - | feedback_TEST_to_OLD (Model_Def.Inc_TEST ((d, ts), penv)) = (Inc ((d, ts), penv))
5.24 + | feedback_TEST_to_OLD (Model_Def.Inc_TEST (d, ts)) = (Inc ((d, ts), (TermC.empty, [])))
5.25 | feedback_TEST_to_OLD (Model_Def.Sup_TEST (d, ts)) = (Sup (d, ts))
5.26 fun TEST_to_OLD i_model =
5.27 map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_TEST_to_OLD e)) i_model
5.28 @@ -164,14 +164,14 @@
5.29 | feedback_to_string _ (Par s) = "Trm "^s;
5.30
5.31 (**)
5.32 -fun feedback_TEST_to_string ctxt (Cor_TEST ((d, ts), _)) =
5.33 +fun feedback_TEST_to_string ctxt (Cor_TEST (d, ts)) =
5.34 "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
5.35 | feedback_TEST_to_string _ (Syn_TEST c) =
5.36 "Syn_TEST " ^ c
5.37 - | feedback_TEST_to_string ctxt (Inc_TEST ((d, []), _)) =
5.38 + | feedback_TEST_to_string ctxt (Inc_TEST (d, [])) =
5.39 "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^
5.40 Model_Pattern.empty_for d
5.41 - | feedback_TEST_to_string ctxt (Inc_TEST ((d, ts), _)) =
5.42 + | feedback_TEST_to_string ctxt (Inc_TEST (d, ts)) =
5.43 "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
5.44 | feedback_TEST_to_string ctxt (Sup_TEST (d, ts)) =
5.45 "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
5.46 @@ -217,7 +217,7 @@
5.47 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of
5.48 NONE => raise ERROR "I_Model.pat_to_item_TEST with NONE"
5.49 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field,
5.50 - (Inc_TEST ((descr, []), (descr, [])), Position.none))
5.51 + (Inc_TEST (descr, []), Position.none))
5.52 fun init_TEST o_model model_patt =
5.53 let
5.54 val pre_items = map (pat_to_item o_model) model_patt
5.55 @@ -242,9 +242,9 @@
5.56 | descriptor (Sup (d, _)) = d
5.57 | descriptor (Mis (d, _)) = d
5.58 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
5.59 -fun descriptor_TEST (Cor_TEST ((d ,_), _)) = d
5.60 +fun descriptor_TEST (Cor_TEST (d ,_)) = d
5.61 | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
5.62 - | descriptor_TEST (Inc_TEST ((d, _), _)) = d
5.63 + | descriptor_TEST (Inc_TEST (d, _)) = d
5.64 | descriptor_TEST (Sup_TEST (d, _)) = d
5.65
5.66 fun descr_pairs_to_string ctxt equal_descr_pairs =
5.67 @@ -532,7 +532,7 @@
5.68 "variants " ^ ints2str' vnts ^ " and descriptor " ^
5.69 (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
5.70 fun transfer_terms (i, vnts, m_field, descr, ts) =
5.71 - (i, vnts, true, m_field, (Cor_TEST ((descr, ts), (TermC.empty, [])), Position.none))
5.72 + (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
5.73 fun fill_method o_model pbl_imod met_patt =
5.74 let
5.75 val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
6.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Wed Sep 20 08:27:21 2023 +0200
6.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Wed Sep 20 11:30:50 2023 +0200
6.3 @@ -140,8 +140,8 @@
6.4
6.5 (*get descriptor of those items which can contribute to Subst.T and Env.T*)
6.6 (* get_dscr: feedback_TEST -> descriptor option*)
6.7 -fun get_dscr' (Cor_TEST ((descr, _), _)) = SOME descr
6.8 - | get_dscr' (Inc_TEST ((descr, _), _)) = SOME descr
6.9 +fun get_dscr' (Cor_TEST (descr, _)) = SOME descr
6.10 + | get_dscr' (Inc_TEST (descr, _)) = SOME descr
6.11 | get_dscr' (Sup_TEST (descr, _)) = SOME descr
6.12 | get_dscr' _ = NONE
6.13 (*other feedback cannot contribute to I_Model.mk_env_TEST and Pre_Conds.mk_env_TEST*)
6.14 @@ -197,12 +197,12 @@
6.15 else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
6.16 else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
6.17
6.18 -fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []
6.19 - | mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) =
6.20 +fun mk_env_model _ (Model_Def.Cor_TEST (_, [])) = []
6.21 + | mk_env_model id (Model_Def.Cor_TEST (descr, ts)) =
6.22 handle_lists id (descr, ts)
6.23 | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
6.24 - | mk_env_model _ (Model_Def.Inc_TEST ((_, []), _)) = []
6.25 - | mk_env_model id (Model_Def.Inc_TEST ((descr, ts), _)) =
6.26 + | mk_env_model _ (Model_Def.Inc_TEST (_, [])) = []
6.27 + | mk_env_model id (Model_Def.Inc_TEST (descr, ts)) =
6.28 handle_lists id (descr, ts)
6.29 | mk_env_model _ (Model_Def.Sup_TEST _) = []
6.30 fun make_env_model equal_descr_pairs =
6.31 @@ -240,9 +240,9 @@
6.32 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
6.33 (*T_TESTnew*)
6.34
6.35 -fun discern_feedback id (Model_Def.Cor_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
6.36 +fun discern_feedback id (Model_Def.Cor_TEST (descr, ts)) = discern_typ id (descr, ts)
6.37 | discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)
6.38 - | discern_feedback id (Model_Def.Inc_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
6.39 + | discern_feedback id (Model_Def.Inc_TEST (descr, ts)) = discern_typ id (descr, ts)
6.40 | discern_feedback _ (Model_Def.Sup_TEST _) = []
6.41 fun make_envs_preconds equal_givens =
6.42 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
7.1 --- a/src/Tools/isac/Specify/refine.sml Wed Sep 20 08:27:21 2023 +0200
7.2 +++ b/src/Tools/isac/Specify/refine.sml Wed Sep 20 11:30:50 2023 +0200
7.3 @@ -86,17 +86,17 @@
7.4 | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
7.5 | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
7.6 (*T_TEST*)
7.7 -fun chk_TEST (_: theory) pbt (i, vats, b, f, I_Model.Cor_TEST ((d, vs), _)) =
7.8 +fun chk_TEST (_: theory) pbt (i, vats, b, f, I_Model.Cor_TEST (d, vs)) =
7.9 (case find_first (eq1 d) pbt of
7.10 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
7.11 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))
7.12 | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))
7.13 - | chk_TEST _ pbt (i, vats, b, f, I_Model.Inc_TEST ((d, vs), _)) =
7.14 + | chk_TEST _ pbt (i, vats, b, f, I_Model.Inc_TEST (d, vs)) =
7.15 (case find_first (eq1 d) pbt of
7.16 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
7.17 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))
7.18 | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))
7.19 | chk_TEST _ pbt (i, vats, b, f, I_Model.Sup_TEST (d, vs)) =
7.20 (case find_first (eq1 d) pbt of
7.21 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST ((d,vs), (id, [Input_Descript.join'''' (d, vs)])))
7.22 + SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))
7.23 | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))
7.24 (*T_TESTnew*)
7.25
8.1 --- a/test/Tools/isac/BridgeJEdit/template.sml Wed Sep 20 08:27:21 2023 +0200
8.2 +++ b/test/Tools/isac/BridgeJEdit/template.sml Wed Sep 20 11:30:50 2023 +0200
8.3 @@ -80,7 +80,7 @@
8.4
8.5 val return_ = (m_field, filter (fn (_, _, _, f, _) => f = m_field) items |>
8.6 map (item_to_out ctxt));
8.7 -"~~~~~ fun item_to_out , args:"; val (ctxt, (_, _, _, _, (I_Model.Inc_TEST ((dsc, []), _), _))) =
8.8 +"~~~~~ fun item_to_out , args:"; val (ctxt, (_, _, _, _, (I_Model.Inc_TEST ((dsc, [])), _))) =
8.9 (ctxt, nth 1 items);
8.10 val return_ = (UnparseC.term ctxt dsc ^ " " ^ Model_Pattern.empty_for dsc, Incomplete)
8.11
9.1 --- a/test/Tools/isac/Interpret/li-tool.sml Wed Sep 20 08:27:21 2023 +0200
9.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Sep 20 11:30:50 2023 +0200
9.3 @@ -401,7 +401,7 @@
9.4 (*////---------------- step into make_env_model --------------------------------------------\\*)
9.5 "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
9.6 "~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
9.7 -"~~~~~ fun mk_env_model , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
9.8 +"~~~~~ fun mk_env_model , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts)))) = (id, feedb);
9.9
9.10 handle_lists id (descr, ts);
9.11 "~~~~~ fun handle_lists , args:"; val (id, (descr, ts)) = (id, (descr, ts));
10.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Wed Sep 20 08:27:21 2023 +0200
10.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Wed Sep 20 11:30:50 2023 +0200
10.3 @@ -188,8 +188,7 @@
10.4 (*!!!*) val patt = equal_descr_pairs |> hd |> #1
10.5 (*!!!*)val equal_descr_pairs =
10.6 (patt,
10.7 - (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term),
10.8 - (TermC.empty, [])), pos)))
10.9 + (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term)), pos)))
10.10 :: tl equal_descr_pairs
10.11 (*for building make_env_s -------------------------------------------------------------------/*)
10.12
10.13 @@ -217,7 +216,7 @@
10.14 (*nth 1 equal_descr_pairs* )
10.15 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
10.16 ( *nth 2 equal_descr_pairs*)
10.17 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts), _))) = (id, feedb);
10.18 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts)))) = (id, feedb);
10.19
10.20 (*nth 1 equal_descr_pairs* )
10.21 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
10.22 @@ -580,7 +579,7 @@
10.23 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) =>
10.24 discern_feedback id feedb)
10.25 val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens;
10.26 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
10.27 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts)))) = (id, feedb);
10.28
10.29 discern_typ id (descr, ts);
10.30 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
11.1 --- a/test/Tools/isac/Specify/pre-conditions.sml Wed Sep 20 08:27:21 2023 +0200
11.2 +++ b/test/Tools/isac/Specify/pre-conditions.sml Wed Sep 20 11:30:50 2023 +0200
11.3 @@ -40,12 +40,10 @@
11.4 (* probl_POS from above, #1 and #2 replaced by complete items, in order to evaluate to true*)
11.5 val probl_POS =
11.6 (1, [1,2,3], true, "#Given",
11.7 - (Cor_TEST ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}]),
11.8 - (@{term "fixes::real"}, [@{term "r::real"}])), Position.none )) ::
11.9 + (Cor_TEST ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}])), Position.none )) ::
11.10 nth 2 probl :: nth 3 probl :: nth 4 probl ::
11.11 (5, [1,2], true, "#Relate",
11.12 - (Cor_TEST ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),
11.13 - (@{term "sideconds::bool list"}, [TermC.empty])), Position.none ))
11.14 + (Cor_TEST ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}])), Position.none ))
11.15 :: [] : I_Model.T_TEST;
11.16 val probl_OLD = I_Model.TEST_to_OLD probl : I_Model.T;
11.17
12.1 --- a/test/Tools/isac/Specify/refine.sml Wed Sep 20 08:27:21 2023 +0200
12.2 +++ b/test/Tools/isac/Specify/refine.sml Wed Sep 20 11:30:50 2023 +0200
12.3 @@ -429,7 +429,7 @@
12.4 make_envs_preconds equal_givens;
12.5 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
12.6 "~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_givens);
12.7 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) =
12.8 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts)))) =
12.9 (id, feedb);
12.10
12.11 val return_discern_typ as [] =
13.1 --- a/test/Tools/isac/Test_Isac.thy Wed Sep 20 08:27:21 2023 +0200
13.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Sep 20 11:30:50 2023 +0200
13.3 @@ -269,7 +269,7 @@
13.4 ML_file "Specify/i-model.sml"
13.5 ML_file "Specify/pre-conditions.sml"
13.6 ML_file "Specify/p-model.sml"
13.7 - ML_file "Specify/m-match.sml"
13.8 + ML_file "Specify/m-match.sml"
13.9 ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
13.10 ML_file "Specify/test-out.sml"
13.11 ML_file "Specify/specify-step.sml"
13.12 @@ -308,7 +308,7 @@
13.13 ML_file "BridgeJEdit/vscode-example.sml"
13.14 (**)
13.15
13.16 - ML_file "Knowledge/delete.sml"
13.17 + ML_file "Knowledge/delete.sml"
13.18 ML_file "Knowledge/descript.sml"
13.19 ML_file "Knowledge/simplify.sml"
13.20 ML_file "Knowledge/poly-1.sml"