1.1 --- a/TODO.md Thu Nov 30 08:11:50 2023 +0100
1.2 +++ b/TODO.md Fri Dec 01 05:51:18 2023 +0100
1.3 @@ -45,8 +45,10 @@
1.4 ***** priority of WN items is top down, most urgent/simple on top
1.5
1.6 * WN:
1.7 +* WN: replace I_Model.descriptor with fun descr_exists: descriptor -> feedback -> bool
1.8 * WN: review Model_Def.is_list_descr, replace by Term.is_list. Exception: make_values
1.9 (values determine handling_lists by [[..], [..], ..])
1.10 +* WN: review Specify.select_inc_lists .. should not be necessary
1.11 * WN: intro-fn into M_Match
1.12 * WN: after--^^^ replace I_Model.descriptor_TEST with Model_Def.get_descr, ELIMI_Model.descriptor
1.13 * WN: thy --> ctxt in by_Add_, ? I_Model.T_TEST ?
2.1 --- a/src/Tools/isac/Build_Isac.thy Thu Nov 30 08:11:50 2023 +0100
2.2 +++ b/src/Tools/isac/Build_Isac.thy Fri Dec 01 05:51:18 2023 +0100
2.3 @@ -289,3 +289,13 @@
2.4
2.5
2.6
2.7 +
2.8 +
2.9 +
2.10 +
2.11 +
2.12 +
2.13 +
2.14 +
2.15 +
2.16 +
3.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Thu Nov 30 08:11:50 2023 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Fri Dec 01 05:51:18 2023 +0100
3.3 @@ -57,6 +57,7 @@
3.4
3.5 val member_vnt: variants -> variant -> bool
3.6 val max_variants: o_model -> i_model_TEST -> variants
3.7 + val max_variants'': i_model_TEST -> variants
3.8
3.9 (*from isac_test for Minisubpbl*)
3.10 val all_variants: ('a * variants * 'c * 'd * 'e) list -> variants
3.11 @@ -220,7 +221,7 @@
3.12 if some_input feedb then 1 else 0) i_model) 0;
3.13 fun arrange_args [] _ = []
3.14 | arrange_args (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args ss (cnt + 1, all))
3.15 -fun max_variants o_model i_model =
3.16 +fun max_variants' i_model =
3.17 let
3.18 val all_variants =
3.19 map (fn (_, variants, _, _, _) => variants) i_model
3.20 @@ -234,12 +235,20 @@
3.21 val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
3.22 |> map snd
3.23 in
3.24 + maxes
3.25 + end
3.26 +fun max_variants o_model i_model =
3.27 + let
3.28 + val maxes = max_variants' i_model
3.29 + in
3.30 if maxes = []
3.31 then map (fn (_, variants, _, _, _) => variants) o_model
3.32 |> flat
3.33 |> distinct op =
3.34 else maxes
3.35 - end
3.36 + end
3.37 +fun max_variants'' [] = raise ERROR "Model_Def.max_variants'' NOT for i_model = []"
3.38 + | max_variants'' i_model = max_variants' i_model
3.39
3.40
3.41 (** definitions for O_Model.T **)
4.1 --- a/src/Tools/isac/Specify/i-model.sml Thu Nov 30 08:11:50 2023 +0100
4.2 +++ b/src/Tools/isac/Specify/i-model.sml Fri Dec 01 05:51:18 2023 +0100
4.3 @@ -223,7 +223,7 @@
4.4 in map pbt2itm pbt end
4.5
4.6 (*
4.7 - Design decision:
4.8 + NEW design decision:
4.9 * Now the Model in Specification is intialised such that the placement of items can be
4.10 maximally stable during interactive input to the Specification.
4.11 * Template.show provides the initial output to the user and thus determines what will be parsed
4.12 @@ -231,21 +231,21 @@
4.13 * The relation between O_Model.T and I_Model.T becomes much simpler.
4.14 *)
4.15 (**)
4.16 -fun pat_to_item ctxt o_model (_, (descriptor, _)) =
4.17 +fun patt_to_item ctxt o_model (_, (descriptor, _)) =
4.18 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of
4.19 - NONE => raise ERROR ("I_Model.pat_to_item NONE for " ^ UnparseC.term ctxt descriptor)
4.20 + NONE => raise ERROR ("I_Model.patt_to_item NONE for " ^ UnparseC.term ctxt descriptor)
4.21 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field,
4.22 (Inc_TEST (descr, []), Position.none))
4.23 fun init_TEST ctxt o_model model_patt =
4.24 let
4.25 - val pre_items = map (pat_to_item ctxt o_model) model_patt
4.26 + val pre_items = map (patt_to_item ctxt o_model) model_patt
4.27 in
4.28 O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))
4.29 end
4.30
4.31
4.32 val unique = Syntax.read_term\<^context> "UnIqE_tErM";
4.33 -(*/-wait for intro-fn into M_Match-\*)
4.34 +(*DANGEROUS: do NOT use "UnIqE_tErM" *)
4.35 fun descriptor (Cor ((d ,_), _)) = d
4.36 | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
4.37 | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)
4.38 @@ -253,7 +253,7 @@
4.39 | descriptor (Sup (d, _)) = d
4.40 | descriptor (Mis (d, _)) = d
4.41 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
4.42 -(*\-wait for intro-fn into M_Match-/*)
4.43 +(*DANGEROUS: do NOT use "UnIqE_tErM" *)
4.44 fun descriptor_TEST (Cor_TEST (d ,_)) = d
4.45 | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
4.46 | descriptor_TEST (Inc_TEST (d, _)) = d
4.47 @@ -515,6 +515,7 @@
4.48 | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*)
4.49 | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*)
4.50
4.51 +(*fill method from items already input*)
4.52 fun fill_method o_model (pbl_imod, met_imod) met_patt =
4.53 let
4.54 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod
5.1 --- a/src/Tools/isac/Specify/m-match.sml Thu Nov 30 08:11:50 2023 +0100
5.2 +++ b/src/Tools/isac/Specify/m-match.sml Fri Dec 01 05:51:18 2023 +0100
5.3 @@ -13,9 +13,12 @@
5.4 val matchs2str : T list -> string
5.5
5.6 val data_by_o: Proof.context -> O_Model.T ->
5.7 - Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set -> bool * (I_Model.T_TEST * Pre_Conds.T)
5.8 + Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set ->
5.9 + bool * (I_Model.T_TEST * Pre_Conds.T)
5.10 val by_o_model: Proof.context -> O_Model.T ->
5.11 Model_Pattern.single list * Pre_Conds.unchecked * Rule_Def.rule_set -> bool
5.12 + val by_i_model: Proof.context -> I_Model.T_TEST ->
5.13 + Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set -> bool * Pre_Conds.T
5.14 val by_i_models: Proof.context -> O_Model.T -> I_Model.T_TEST * I_Model.T_TEST ->
5.15 Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set ->
5.16 bool * (I_Model.T_TEST * Pre_Conds.T)
5.17 @@ -29,7 +32,7 @@
5.18
5.19 (*from isac_test for Minisubpbl*)
5.20 val chk1_: Model_Pattern.T -> O_Model.single -> I_Model.T
5.21 - val contains_d: Model_Def.descriptor -> O_Model.T -> bool
5.22 + val contains_o: Model_Def.descriptor -> O_Model.T -> bool
5.23
5.24 \<^isac_test>\<open>
5.25 val matc: theory -> Model_Pattern.T -> term list -> O_Model.T -> O_Model.T
5.26 @@ -49,7 +52,7 @@
5.27 | match2str (NoMatch (pI, model)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string model ^ ")";
5.28 fun matchs2str ms = (strs2str o (map match2str)) ms;
5.29
5.30 -fun contains_d descr o_model =
5.31 +fun contains_o descr o_model =
5.32 case find_first (fn (_, _, _, descr', _) => descr' = descr) o_model of
5.33 SOME _ => true | NONE => false
5.34 fun data_by_o ctxt o_model (model_patt, where_, where_rls) =
5.35 @@ -59,7 +62,7 @@
5.36 => if member_swap op = 1 (*variant 1 is mandatory*) variants then [o_single] else [])
5.37 |> flat
5.38 val is_complete = model_patt
5.39 - |> map (fn (_, (descr, _)) => contains_d descr o_model_vnt)
5.40 + |> map (fn (_, (descr, _)) => contains_o descr o_model_vnt)
5.41 |> curry (foldl and_) true
5.42 val i_model = (*in order to match sig of Pre_Conds.check*)
5.43 map (fn (a, b, c, d, e) => (a, b, true, c, (I_Model.Cor_TEST (d, e), Position.none))) o_model_vnt
5.44 @@ -79,6 +82,25 @@
5.45 (check, (met_imod, preconds))
5.46 end
5.47
5.48 +(*contains_i: descriptor -> I_Model.T_TEST -> bool*)
5.49 +fun contains_i descr i_model =
5.50 + case find_first (fn (_, _, _, _, (feedb, _)) => Model_Def.get_descr feedb = descr) i_model of
5.51 + SOME _ => true | NONE => false
5.52 +fun by_i_model ctxt i_model (model_patt, where_, where_rls) =
5.53 + let
5.54 + val max_vnt = last_elem (Model_Def.max_variants'' i_model)
5.55 + val i_model_vnt = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) i_model
5.56 + val is_complete = model_patt
5.57 + |> map (fn (_, (descr, _)) => contains_i descr i_model_vnt)
5.58 + |> curry (foldl and_) true
5.59 +
5.60 + val (env_model, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model_vnt;
5.61 + val (prec_check, precs)
5.62 + = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
5.63 + in
5.64 + (is_complete andalso prec_check, precs)
5.65 + end
5.66 +
5.67
5.68 (** for use by math-authors **)
5.69
6.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Thu Nov 30 08:11:50 2023 +0100
6.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Fri Dec 01 05:51:18 2023 +0100
6.3 @@ -141,7 +141,7 @@
6.4 let
6.5 val equal_descr =
6.6 filter (fn i_single => case get_descr_opt i_single of
6.7 - NONE => false (*--------vvvvv*)
6.8 + NONE => false
6.9 | SOME descr' => descr' = descr) i_model
6.10 in
6.11 (map (pair m_patt_single) equal_descr)
7.1 --- a/src/Tools/isac/Specify/refine.sml Thu Nov 30 08:11:50 2023 +0100
7.2 +++ b/src/Tools/isac/Specify/refine.sml Fri Dec 01 05:51:18 2023 +0100
7.3 @@ -61,110 +61,27 @@
7.4
7.5 fun is_matches_ (Match_ _) = true
7.6 | is_matches_ _ = false;
7.7 -
7.8 fun match_found ms = ((find_first is_matches_) o rev) ms;
7.9
7.10 -fun eq1 d (_, (d', _)) = (d = d');
7.11 -
7.12 -(* chk_: theory -> ('a * (term * term)) list -> I_Model.single -> I_Model.single*)
7.13 -(*T_TESTold*)
7.14 -fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
7.15 - (case find_first (eq1 d) pbt of
7.16 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
7.17 - | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
7.18 - | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
7.19 - (case find_first (eq1 d) pbt of
7.20 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
7.21 - | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
7.22 - | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
7.23 - | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
7.24 - | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
7.25 - (case find_first (eq1 d) pbt of
7.26 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, [Input_Descript.join'''' (d, vs)])))
7.27 - | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
7.28 - | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
7.29 - (case find_first (eq1 d) pbt of
7.30 - SOME _ =>
7.31 - raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Input_Descript.join'''' d vs))):itm)"
7.32 - | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
7.33 - | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
7.34 -(*T_TEST*)
7.35 -fun chk_TEST (_: theory) pbt (i, vats, b, f, I_Model.Cor_TEST (d, vs)) =
7.36 - (case find_first (eq1 d) pbt of
7.37 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))
7.38 - | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))
7.39 - | chk_TEST _ pbt (i, vats, b, f, I_Model.Inc_TEST (d, vs)) =
7.40 - (case find_first (eq1 d) pbt of
7.41 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))
7.42 - | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))
7.43 - | chk_TEST _ pbt (i, vats, b, f, I_Model.Sup_TEST (d, vs)) =
7.44 - (case find_first (eq1 d) pbt of
7.45 - SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))
7.46 - | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))
7.47 -(*T_TESTnew*)
7.48 -
7.49 -fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
7.50 -fun eq0 (0, _, _, _, _) = true
7.51 - | eq0 _ = false;
7.52 -fun max_i i [] = i
7.53 - | max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;
7.54 -fun max_id [] = 0
7.55 - | max_id ((id, _, _, _, _) :: is) = max_i id is;
7.56 -fun add_idvat itms _ _ [] = itms
7.57 - | add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =
7.58 - add_idvat (itms @ [(i, [], b, f, itm_)]) (i + 1) mvat its;
7.59 -
7.60 -(* find elements of pbt not contained in itms;
7.61 - if such one is untouched, return this one, otherwise create new itm *)
7.62 -fun chk_m itms untouched (p as (f, (d, id))) =
7.63 - case find_first (eq2 p) itms of
7.64 - SOME _ => []
7.65 - | NONE =>
7.66 - (case find_first (eq2 p) untouched of
7.67 - SOME itm => [itm]
7.68 - | NONE => [(0, [], false, f, I_Model.Mis (d, id))]);
7.69 -
7.70 -fun chk_mis mvat itms untouched pbt =
7.71 - let val mis = (flat o (map (chk_m itms untouched))) pbt;
7.72 - val mid = max_id itms;
7.73 - in add_idvat [] (mid + 1) mvat mis end;
7.74 -
7.75 -(*
7.76 - check a problem (ie. i?model) for matching a problemtype,
7.77 - takes the Pre_Conds.max_variant for concluding completeness
7.78 -*)
7.79 -(* match_itms: theory -> I_Model.T -> Model_Pattern.T * unchecked * Rule_Def.rule_set ->
7.80 - bool * (I_Model.T * (bool * term) list)*)
7.81 -fun match_itms thy itms (pbt, where_, where_rls) =
7.82 - let
7.83 - fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
7.84 - val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
7.85 - val mvat = Pre_Conds.max_variant itms';
7.86 - val itms'' = filter (okv mvat) itms';
7.87 - val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
7.88 - val mis = chk_mis mvat itms'' untouched pbt;
7.89 - val (pb, where_') = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_
7.90 - (pbt, I_Model.OLD_to_TEST itms'')
7.91 - in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
7.92 -
7.93 (* version for tactic Refine_Problem *)
7.94 fun find_match _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
7.95 let
7.96 val {thy, model, where_, where_rls, ...} = py
7.97 - (*TODO val where_ = map TermC.adapt_to_type where_ ... adapt to current ctxt*)
7.98 - val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
7.99 + val ctxt = Proof_Context.init_global thy
7.100 + val (b, where_') = M_Match.by_i_model ctxt (I_Model.OLD_to_TEST itms) (model, where_, where_rls);
7.101 in
7.102 if b
7.103 - then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', where_'))]
7.104 + then pbls @ [Match_ (rev (pblRD @ [pI]), (itms, where_'))]
7.105 else pbls @ [NoMatch_]
7.106 end
7.107 | find_match _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
7.108 let
7.109 val {thy, model, where_, where_rls, ...} = py
7.110 - val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
7.111 - in if b
7.112 - then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', where_'))
7.113 - in find_matchs thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
7.114 + val ctxt = Proof_Context.init_global thy
7.115 + val (b, where_') = M_Match.by_i_model ctxt (I_Model.OLD_to_TEST itms) (model, where_, where_rls);
7.116 + in if b then
7.117 + let val pbl = Match_ (rev (pblRD @ [pI]), (itms, where_'))
7.118 + in find_matchs thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
7.119 else (pbls @ [NoMatch_])
7.120 end
7.121 | find_match _ _ _ _ _ = raise ERROR "find_match: uncovered fun def."
7.122 @@ -181,12 +98,11 @@
7.123 case match_found ((Store.apply (get_pbls ())) (find_match thy ((rev o tl) pblID) itms [])
7.124 pblID (rev pblID)) of
7.125 NONE => NONE
7.126 - | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd;
7.127 + | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd
7.128 + | _ => raise ERROR "Refine.problem: undef. args";
7.129
7.130 -(*
7.131 - refine a problem; construct pblRD while scanning Problem.T Store.T
7.132 -TODO: as \<open>check_match: 'a -> .. -> 'b option\<close> could be ignorant of Store.T structure.
7.133 -*)
7.134 +(* refine a problem; construct pblRD while scanning Problem.T Store.T*)
7.135 +(*TODO: as \<open>check_match: 'a -> .. -> 'b option\<close> could be ignorant of Store.T structure.*)
7.136 fun check_match ctxt pblRD ori (Store.Node (pI, [py], [])) =
7.137 let
7.138 val {where_rls, model, where_, ...} = py: Problem.T
8.1 --- a/src/Tools/isac/Specify/specify.sml Thu Nov 30 08:11:50 2023 +0100
8.2 +++ b/src/Tools/isac/Specify/specify.sml Fri Dec 01 05:51:18 2023 +0100
8.3 @@ -30,7 +30,7 @@
8.4
8.5 fun select_inc_lists i_model =
8.6 let
8.7 - (* filter problem with Const ("Input_Descript.solutions", _) *)
8.8 + (* filter problem like with Const ("Input_Descript.solutions", _) *)
8.9 val filt = (fn (_, _, _, _, (I_Model.Inc_TEST (descr, _::_) , _)) => Model_Def.is_list_descr descr
8.10 | _ => false)
8.11 in
9.1 --- a/test/Tools/isac/Specify/m-match.sml Thu Nov 30 08:11:50 2023 +0100
9.2 +++ b/test/Tools/isac/Specify/m-match.sml Fri Dec 01 05:51:18 2023 +0100
9.3 @@ -42,7 +42,7 @@
9.4 |> map (fn o_single as (_, variants, _, _, _)
9.5 => if member_swap op = 1 (*variant 1 is mandatory*) variants then [o_single] else [])
9.6 |> flat
9.7 - val is_complete as true = map (fn (_, (descr, _)) => contains_d descr o_model_vnt) model_patt
9.8 + val is_complete as true = map (fn (_, (descr, _)) => contains_o descr o_model_vnt) model_patt
9.9 |> curry (foldl and_) true
9.10 val i_model = (*in order to match sig of Pre_Conds.check*)
9.11 map (fn (a, b, c, d, e) => (a, b, true, c, (I_Model.Cor_TEST (d, e), Position.none))) o_model_vnt
9.12 @@ -54,8 +54,6 @@
9.13
9.14 val return_by_o_model as true = (data_by_o ctxt o_model (model_patt, where_, where_rls)) |> #1;
9.15
9.16 -(*//------------------ setup test data for fun by_o_model 2 --------------------------------\\*)
9.17 -(*\\------------------ setup test data for fun by_o_model 2 --------------------------------//*)
9.18
9.19 (*** ------- fun by_formalise ------------------------------------------------------------------ ***)
9.20 "----------- fun by_formalise ---------------------------------------------------------------------";
10.1 --- a/test/Tools/isac/Specify/refine.sml Thu Nov 30 08:11:50 2023 +0100
10.2 +++ b/test/Tools/isac/Specify/refine.sml Fri Dec 01 05:51:18 2023 +0100
10.3 @@ -385,7 +385,7 @@
10.4 => if member_swap op = 1 (*variant 1 is mandatory*) variants then [o_single] else [])
10.5 |> flat
10.6 val is_complete = model_patt
10.7 - |> map (fn (_, (descr, _)) => contains_d descr o_model_vnt)
10.8 + |> map (fn (_, (descr, _)) => contains_o descr o_model_vnt)
10.9 |> curry (foldl and_) true
10.10 val i_model = (*in order to match sig of Pre_Conds.check*)
10.11 map (fn (a, b, c, d, e) => (a, b, true, c, (I_Model.Cor_TEST (d, e), Position.none))) o_model_vnt
11.1 --- a/test/Tools/isac/Test_Theory.thy Thu Nov 30 08:11:50 2023 +0100
11.2 +++ b/test/Tools/isac/Test_Theory.thy Fri Dec 01 05:51:18 2023 +0100
11.3 @@ -205,9 +205,17 @@
11.4 \<close> ML \<open>
11.5 \<close>
11.6
11.7 -ML_file "Specify/refine.sml"
11.8 +(** )ML_file "$ISABELLE_ISAC/Specify/refine.sml"( **)
11.9 section \<open>===================================================================================\<close>
11.10 -section \<open>===== new code ============================================================================\<close>
11.11 +section \<open>===== new code xxxxx ==============================================================\<close>
11.12 +ML \<open>
11.13 +\<close> ML \<open>
11.14 +
11.15 +\<close> ML \<open>
11.16 +\<close>
11.17 +
11.18 +section \<open>===================================================================================\<close>
11.19 +section \<open>===== ============================================================================\<close>
11.20 ML \<open>
11.21 \<close> ML \<open>
11.22