1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Sat May 16 16:23:24 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Sat May 16 16:54:39 2020 +0200
1.3 @@ -236,7 +236,7 @@
1.4 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
1.5 \ --> m' <= m)))"],
1.6 relate=["max_relation r","additionalRels rs"]}:string ppc;
1.7 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.8 +val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.9 "coil";
1.10 val org = ["fixed_values [R=(R::real)]",
1.11 "bound_variable a", "bound_variable b", "bound_variable alpha",
1.12 @@ -258,7 +258,7 @@
1.13 relate=["max_relation (A=#2*a*b - a^^^#2)",
1.14 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.15 }: string ppc;
1.16 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.17 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.18
1.19 "met --- maximum_by_differentiation ---";
1.20 val met = {given=["fixed_values (cs::bool list)","bound_variable v",
1.21 @@ -274,7 +274,7 @@
1.22 \( ALL x. lower_bound <= x & x <= upper_bound \
1.23 \ --> (%v. t) x <= m)"],
1.24 relate=["rs::bool list"]}: string ppc;
1.25 -val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
1.26 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
1.27
1.28
1.29 "pbltyp --- make_fun ---";
1.30 @@ -285,27 +285,27 @@
1.31 where_=[],
1.32 find=["function_term t"],with_=[(*???*)],
1.33 relate=[(*???*)]}: string ppc;
1.34 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.35 +val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.36 "coil";
1.37 val pbl = {given=["equality (A=#2*a*b - a^^^#2)","bound_variable alpha",
1.38 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.39 where_=[],
1.40 find=["function_term t"],
1.41 with_=[],relate=[]}: string ppc;
1.42 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.43 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.44
1.45 "met --- make_explicit_and_substitute ---";
1.46 val met = {given=["equality e","bound_variable v", "equalities es"],
1.47 where_=[],
1.48 find=["function_term t"],with_=[(*???*)],
1.49 relate=[(*???*)]}: string ppc;
1.50 -val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.51 +val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
1.52 "met --- introduce_a_new_variable ---";
1.53 val met = {given=["equality e","bound_variable v", "substitutions es"],
1.54 where_=[],
1.55 find=["function_term t"],with_=[(*???*)],
1.56 relate=[(*???*)]}: string ppc;
1.57 -val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.58 +val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
1.59
1.60
1.61 "pbltyp --- max_of_fun_on_interval ---";
1.62 @@ -317,13 +317,13 @@
1.63 \ (ALL x::real. lower_bound <= x & x <= upper_bound \
1.64 \ --> (%v. t) x <= m)"],
1.65 relate=[]}: string ppc;
1.66 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.67 +val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
1.68 "coil";
1.69 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
1.70 \ (#2*R*sin alpha)^^^#2","bound_variable alpha",
1.71 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
1.72 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
1.73 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.74 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
1.75
1.76
1.77 (* pbltyp --- max_of_fun --- *)
1.78 @@ -345,22 +345,22 @@
1.79 val org = {given=["[u=(#12::real)]"],where_=[],
1.80 find=["[a,(b::real)]"],with_=[],
1.81 relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
1.82 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.83 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.84 "p.116";
1.85 val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
1.86 find=["[x,(y::real)]"],with_=[],
1.87 relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
1.88 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.89 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.90 "p.117";
1.91 val org = {given=["[r=#5]"],where_=[],
1.92 find=["[x,(y::real)]"],with_=[],
1.93 relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
1.94 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.95 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.96 "#241";
1.97 val org = {given=["[s=(#10::real)]"],where_=[],
1.98 find=["[p::real]"],with_=[],
1.99 relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
1.100 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.101 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
1.102
1.103 (*
1.104 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
2.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Sat May 16 16:23:24 2020 +0200
2.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Sat May 16 16:54:39 2020 +0200
2.3 @@ -20,7 +20,7 @@
2.4 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
2.5 \ --> m' <= m)))"*)],
2.6 relate=["max_relation r","additionalRels rs"]}:string ppc;
2.7 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
2.8 +val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
2.9 "coil";
2.10 val org = ["fixedValues [R=(R::real)]",
2.11 "boundVariable a","boundVariable b","boundVariable alpha",
2.12 @@ -44,7 +44,7 @@
2.13 \ --> A' <= A)"*)],
2.14 relate=["relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"]
2.15 }: string ppc;
2.16 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
2.17 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
2.18
2.19 "met --- maximum_by_differentiation ---";
2.20 val met = {given=["fixedValues (cs::bool list)","boundVariable v",
2.21 @@ -62,7 +62,7 @@
2.22 \ --> (%v. t) x <= m)"*)],
2.23 relate=["max_relation mr",
2.24 "additionalRels ars"]}: string ppc;
2.25 -val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
2.26 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
2.27
2.28 "data --- maximum_by_differentiation ---";
2.29 val met = {given=["fixedValues [R=(R::real)]","boundVariable alpha",
2.30 @@ -83,7 +83,7 @@
2.31 \ (%alpha. t) x <= A)"*)],
2.32 relate=["max_relation mr",
2.33 "additionalRels ars"]}: string ppc;
2.34 -val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
2.35 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met;
2.36
2.37 val (SOME ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a^^^#2)";
2.38
2.39 @@ -95,27 +95,27 @@
2.40 where_=[],
2.41 find=["functionTerm t"],with_=[(*???*)],
2.42 relate=[(*???*)]}: string ppc;
2.43 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
2.44 +val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
2.45 "coil";
2.46 val pbl = {given=["equality (A=#2*a*b - a^^^#2)","boundVariable alpha",
2.47 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
2.48 where_=[],
2.49 find=["functionTerm t"],
2.50 with_=[],relate=[]}: string ppc;
2.51 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
2.52 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
2.53
2.54 "met --- make_explicit_and_substitute ---";
2.55 val met = {given=["equality e","boundVariable v", "equalities es"],
2.56 where_=[],
2.57 find=["functionTerm t"],with_=[(*???*)],
2.58 relate=[(*???*)]}: string ppc;
2.59 -val chkmet = ((map (the o (parse thy))) o ppc2list) met;
2.60 +val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
2.61 "met --- introduce_a_new_variable ---";
2.62 val met = {given=["equality e","boundVariable v", "substitutions es"],
2.63 where_=[],
2.64 find=["functionTerm t"],with_=[(*???*)],
2.65 relate=[(*???*)]}: string ppc;
2.66 -val chkmet = ((map (the o (parse thy))) o ppc2list) met;
2.67 +val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met;
2.68
2.69
2.70 "pbltyp --- max_of_fun_on_interval ---";
2.71 @@ -128,13 +128,13 @@
2.72 \ (ALL x::real. lower_bound <= x & x <= upper_bound \
2.73 \ --> (%v. t) x <= m)"*)],
2.74 relate=[]}: string ppc;
2.75 -val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
2.76 +val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp;
2.77 "coil";
2.78 val pbl = {given=["functionTerm (f = #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
2.79 \ (#2*R*sin alpha)^^^#2)","boundVariable alpha",
2.80 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
2.81 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
2.82 -val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
2.83 +val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl;
2.84
2.85
2.86 (* pbltyp --- max_of_fun --- *)
2.87 @@ -150,22 +150,22 @@
2.88 val org = {given=["[u=(#12::real)]"],where_=[],
2.89 find=["[a,(b::real)]"],with_=[],
2.90 relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
2.91 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
2.92 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
2.93 "p.116";
2.94 val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
2.95 find=["[x,(y::real)]"],with_=[],
2.96 relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
2.97 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
2.98 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
2.99 "p.117";
2.100 val org = {given=["[r=#5]"],where_=[],
2.101 find=["[x,(y::real)]"],with_=[],
2.102 relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
2.103 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
2.104 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
2.105 "#241";
2.106 val org = {given=["[s=(#10::real)]"],where_=[],
2.107 find=["[p::real]"],with_=[],
2.108 relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
2.109 -val chkorg = ((map (the o (parse thy))) o ppc2list) org;
2.110 +val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org;
2.111
2.112
2.113
3.1 --- a/src/Tools/isac/Specify/p-model.sml Sat May 16 16:23:24 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/p-model.sml Sat May 16 16:54:39 2020 +0200
3.3 @@ -17,8 +17,11 @@
3.4 type 'a ppc (*shall be dropped with PIDE*)
3.5
3.6 val from : theory -> I_Model.T -> Pre_Conds.T -> T
3.7 +
3.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.9 - (* NONE *)
3.10 + val to_list: 'a ppc -> 'a list
3.11 + val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
3.12 + val mk_additem: string -> TermC.as_string -> Tactic.input
3.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.14 val item_from_feedback: theory -> I_Model.feedback -> item
3.15 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.16 @@ -94,4 +97,16 @@
3.17 val gfr = coll empty itms;
3.18 in add_where gfr (map boolterm2item pre) end;
3.19
3.20 +fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)
3.21 + | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_)
3.22 + | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_)
3.23 + | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
3.24 +fun mk_additem "#Given" ct = Tactic.Add_Given ct
3.25 + | mk_additem "#Find" ct = Tactic.Add_Find ct
3.26 + | mk_additem "#Relate"ct = Tactic.Add_Relation ct
3.27 + | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
3.28 +
3.29 +fun to_list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
3.30 + gis @ whs @ fis @ wis @ res
3.31 +
3.32 (**)end(**);
3.33 \ No newline at end of file
4.1 --- a/src/Tools/isac/Specify/specification.sml Sat May 16 16:23:24 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/specification.sml Sat May 16 16:54:39 2020 +0200
4.3 @@ -86,12 +86,6 @@
4.4 val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
4.5 ( *\------- to Specify from Specification -------/*)
4.6
4.7 -(*/------- to P_Model from Specification -------\*)
4.8 - val ppc2list: 'a P_Model.ppc -> 'a list
4.9 - val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
4.10 - val mk_additem: string -> TermC.as_string -> Tactic.input
4.11 -(*\------- to P_Model from Specification -------/*)
4.12 -
4.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.14 (*NONE*)
4.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.16 @@ -126,9 +120,6 @@
4.17 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
4.18 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
4.19
4.20 -fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
4.21 - gis @ whs @ fis @ wis @ res
4.22 -
4.23 (* get the number of variants in a problem in 'original',
4.24 assumes equal descriptions in immediate sequence *)
4.25 fun variants_in ts =
4.26 @@ -225,15 +216,6 @@
4.27 | SOME ori => SOME (geti_ct thy ori (hd icl))
4.28 end
4.29
4.30 -fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)
4.31 - | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_)
4.32 - | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_)
4.33 - | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
4.34 -fun mk_additem "#Given" ct = Tactic.Add_Given ct
4.35 - | mk_additem "#Find" ct = Tactic.Add_Find ct
4.36 - | mk_additem "#Relate"ct = Tactic.Add_Relation ct
4.37 - | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")
4.38 -
4.39 (*/------- to Specify from Specification -------\*)
4.40 (*
4.41 TODO: unify with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met
4.42 @@ -256,10 +238,10 @@
4.43 else
4.44 case find_first (I_Model.is_error o #5) pbl of
4.45 SOME (_, _, _, fd, itm_) =>
4.46 - (Pos.Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
4.47 + (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
4.48 | NONE =>
4.49 (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
4.50 - SOME (fd, ct') => (Pos.Pbl, mk_additem fd ct')
4.51 + SOME (fd, ct') => (Pos.Pbl, P_Model.mk_additem fd ct')
4.52 | NONE => (*pbl-items complete*)
4.53 if not preok then (Pos.Pbl, Tactic.Refine_Problem pI')
4.54 else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
4.55 @@ -267,17 +249,17 @@
4.56 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')
4.57 else
4.58 case find_first (I_Model.is_error o #5) met of
4.59 - SOME (_, _, _, fd, itm_) => (Pos.Met, mk_delete (ThyC.get_theory dI) fd itm_)
4.60 + SOME (_, _, _, fd, itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_)
4.61 | NONE =>
4.62 (case nxt_add (ThyC.get_theory dI) oris mpc met of
4.63 - SOME (fd, ct') => (Pos.Met, mk_additem fd ct') (*30.8.01: pre?!?*)
4.64 + SOME (fd, ct') => (Pos.Met, P_Model.mk_additem fd ct') (*30.8.01: pre?!?*)
4.65 | NONE => (Pos.Met, Tactic.Apply_Method mI))))
4.66 | nxt_spec Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
4.67 (case find_first (I_Model.is_error o #5) met of
4.68 - SOME (_,_,_,fd,itm_) => (Pos.Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
4.69 + SOME (_,_,_,fd,itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
4.70 | NONE =>
4.71 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
4.72 - SOME (fd,ct') => (Pos.Met, mk_additem fd ct')
4.73 + SOME (fd,ct') => (Pos.Met, P_Model.mk_additem fd ct')
4.74 | NONE =>
4.75 (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI')
4.76 else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI')
5.1 --- a/src/Tools/isac/Specify/specify.sml Sat May 16 16:23:24 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/specify.sml Sat May 16 16:54:39 2020 +0200
5.3 @@ -47,11 +47,11 @@
5.4 else
5.5 case find_first (I_Model.is_error o #5) pbl of
5.6 SOME (_, _, _, fd, itm_) =>
5.7 - ("dummy", (Pbl, Specification.mk_delete (ThyC.get_theory
5.8 + ("dummy", (Pbl, P_Model.mk_delete (ThyC.get_theory
5.9 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
5.10 | NONE =>
5.11 (case Specification.nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
5.12 - SOME (fd, ct') => ("dummy", (Pbl, Specification.mk_additem fd ct'))
5.13 + SOME (fd, ct') => ("dummy", (Pbl, P_Model.mk_additem fd ct'))
5.14 | NONE => (*pbl-items complete*)
5.15 if not preok then ("dummy", (Pbl, Tactic.Refine_Problem pI'))
5.16 else if dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
5.17 @@ -59,17 +59,17 @@
5.18 else if mI = Method.id_empty then ("dummy", (Pbl, Tactic.Specify_Method mI'))
5.19 else
5.20 case find_first (I_Model.is_error o #5) met of
5.21 - SOME (_, _, _, fd, itm_) => ("dummy", (Met, Specification.mk_delete (ThyC.get_theory dI) fd itm_))
5.22 + SOME (_, _, _, fd, itm_) => ("dummy", (Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_))
5.23 | NONE =>
5.24 (case Specification.nxt_add (ThyC.get_theory dI) oris mpc met of
5.25 - SOME (fd, ct') => ("dummy", (Met, Specification.mk_additem fd ct')) (*30.8.01: pre?!?*)
5.26 + SOME (fd, ct') => ("dummy", (Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*)
5.27 | NONE => ("dummy", (Met, Tactic.Apply_Method mI)))))
5.28 | Met =>
5.29 (case find_first (I_Model.is_error o #5) met of
5.30 - SOME (_,_,_,fd,itm_) => ("dummy", (Met, Specification.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
5.31 + SOME (_,_,_,fd,itm_) => ("dummy", (Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
5.32 | NONE =>
5.33 case Specification.nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
5.34 - SOME (fd,ct') => ("dummy", (Met, Specification.mk_additem fd ct'))
5.35 + SOME (fd,ct') => ("dummy", (Met, P_Model.mk_additem fd ct'))
5.36 | NONE =>
5.37 (if dI = ThyC.id_empty then ("dummy", (Met, Tactic.Specify_Theory dI'))
5.38 else if pI = Problem.id_empty then ("dummy", (Met, Tactic.Specify_Problem pI'))
6.1 --- a/test/Tools/isac/Knowledge/diff.sml Sat May 16 16:23:24 2020 +0200
6.2 +++ b/test/Tools/isac/Knowledge/diff.sml Sat May 16 16:54:39 2020 +0200
6.3 @@ -36,7 +36,7 @@
6.4 Find =["derivative f_f'"],
6.5 With =[],
6.6 Relate=[]}:string ppc;
6.7 -val chkpbt = ((map (the o (parse thy))) o ppc2list) pbt;
6.8 +val chkpbt = ((map (the o (parse thy))) o P_Model.to_list) pbt;
6.9
6.10 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
6.11 "differentiateFor x","derivative f_f'"];
7.1 --- a/test/Tools/isac/Knowledge/integrate.sml Sat May 16 16:23:24 2020 +0200
7.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sat May 16 16:54:39 2020 +0200
7.3 @@ -328,7 +328,7 @@
7.4 Find =["antiDerivative F_F"],
7.5 With =[],
7.6 Relate=[]}:string ppc;
7.7 -val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
7.8 +val chkmodel = ((map (the o (parse thy))) o P_Model.to_list) model;
7.9 val t1 = (Thm.term_of o hd) chkmodel;
7.10 val t2 = (Thm.term_of o hd o tl) chkmodel;
7.11 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
7.12 @@ -340,7 +340,7 @@
7.13 Find =["antiDerivativeName F_F"],
7.14 With =[],
7.15 Relate=[]}:string ppc;
7.16 -val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
7.17 +val chkmodel = ((map (the o (parse thy))) o P_Model.to_list) model;
7.18 val t1 = (Thm.term_of o hd) chkmodel;
7.19 val t2 = (Thm.term_of o hd o tl) chkmodel;
7.20 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;