1.1 --- a/src/Tools/isac/FE-interface/interface.sml Fri Aug 20 12:25:37 2010 +0200
1.2 +++ b/src/Tools/isac/FE-interface/interface.sml Fri Aug 20 14:58:43 2010 +0200
1.3 @@ -420,7 +420,7 @@
1.4 "thy_" =>
1.5 (* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify");
1.6 *)
1.7 - if member op = p_ [Pbl,Met]
1.8 + if member op = [Pbl,Met] p_
1.9 then message2xml cI "thy-context not to calchead"
1.10 else if ip = ([],Res) then message2xml cI "no thy-context at result"
1.11 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
1.12 @@ -492,7 +492,7 @@
1.13 *)
1.14 (let val ((pt, _), _) = get_calc cI
1.15 val ip as (_, p_) = get_pos cI 1
1.16 - in if member op = p_ [Pbl,Met]
1.17 + in if member op = [Pbl,Met] p_
1.18 then let val (pt, chd) = set_method mI (pt, ip)
1.19 in (upd_calc cI ((pt, ip), []);
1.20 modifycalcheadOK2xml cI chd) end
1.21 @@ -506,7 +506,7 @@
1.22 fun setProblem (cI:calcID) (pI:pblID) =
1.23 (let val ((pt, _), _) = get_calc cI
1.24 val ip as (_, p_) = get_pos cI 1
1.25 - in if member op = p_ [Pbl,Met]
1.26 + in if member op = [Pbl,Met] p_
1.27 then let val (pt, chd) = set_problem pI (pt, ip)
1.28 in (upd_calc cI ((pt, ip), []);
1.29 modifycalcheadOK2xml cI chd) end
1.30 @@ -520,7 +520,7 @@
1.31 fun setTheory (cI:calcID) (tI:thyID) =
1.32 (let val ((pt, _), _) = get_calc cI
1.33 val ip as (_, p_) = get_pos cI 1
1.34 - in if member op = p_ [Pbl,Met]
1.35 + in if member op = [Pbl,Met] p_
1.36 then let val (pt, chd) = set_theory tI (pt, ip)
1.37 in (upd_calc cI ((pt, ip), []);
1.38 modifycalcheadOK2xml cI chd) end
1.39 @@ -737,7 +737,7 @@
1.40 val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1,1], Frm));
1.41 *)
1.42 fun initContext (cI:calcID) Thy_ (pos as (p,p_):pos') =
1.43 - ((if member op = p_ [Pbl,Met]
1.44 + ((if member op = [Pbl,Met] p_
1.45 then message2xml cI "thy-context not to calchead"
1.46 else if pos = ([],Res) then message2xml cI "no thy-context at result"
1.47 else let val cs as (ptp as (pt,_),_) = get_calc cI
1.48 @@ -799,7 +799,7 @@
1.49 fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
1.50 (case (implode o (take_fromto 1 4) o explode) guh of
1.51 "thy_" =>
1.52 - if member op = p_ [Pbl,Met]
1.53 + if member op = [Pbl,Met] p_
1.54 then message2xml cI "thy-context not to calchead"
1.55 else if pos = ([],Res) then message2xml cI "no thy-context at result"
1.56 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
2.1 --- a/src/Tools/isac/IsacKnowledge/Atools.ML Fri Aug 20 12:25:37 2010 +0200
2.2 +++ b/src/Tools/isac/IsacKnowledge/Atools.ML Fri Aug 20 14:58:43 2010 +0200
2.3 @@ -60,7 +60,7 @@
2.4 (*-------------------------functions---------------------*)
2.5 local (* rlang 09.02 *)
2.6 (*.a 'c is coefficient of v' if v does occur in c.*)
2.7 - fun coeff_in v c = member op = v (vars c);
2.8 + fun coeff_in v c = member op = (vars c) v;
2.9 in
2.10 fun occurs_in v t = coeff_in v t;
2.11 end;
3.1 --- a/src/Tools/isac/IsacKnowledge/EqSystem.ML Fri Aug 20 12:25:37 2010 +0200
3.2 +++ b/src/Tools/isac/IsacKnowledge/EqSystem.ML Fri Aug 20 14:58:43 2010 +0200
3.3 @@ -90,10 +90,10 @@
3.4 let
3.5 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
3.6 val _=writeln("t= f@ts= \""^
3.7 - ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
3.8 + ((string_of_cterm o (Thm.cterm thy)) f)^"\" @ \"["^
3.9 (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
3.10 val _=writeln("u= g@us= \""^
3.11 - ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
3.12 + ((string_of_cterm o (Thm.cterm thy)) g)^"\" @ \"["^
3.13 (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
3.14 val _=writeln("size_of_term(t,u)= ("^
3.15 (string_of_int(size_of_term' t))^", "^
4.1 --- a/src/Tools/isac/IsacKnowledge/Poly.ML Fri Aug 20 12:25:37 2010 +0200
4.2 +++ b/src/Tools/isac/IsacKnowledge/Poly.ML Fri Aug 20 14:58:43 2010 +0200
4.3 @@ -52,7 +52,7 @@
4.4 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
4.5 fun is_polyrat_in t v =
4.6 let
4.7 - fun coeff_in c v = member op = v (vars c);
4.8 + fun coeff_in c v = member op = (vars c) v;
4.9 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")
4.10 (* at the moment there is no term like this, but ....*)
4.11 | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = not(coeff_in b v)
4.12 @@ -74,7 +74,7 @@
4.13
4.14 local
4.15 (*.a 'c is coefficient of v' if v does NOT occur in c.*)
4.16 - fun coeff_in c v = not (member op = v (vars c));
4.17 + fun coeff_in c v = not (member op = (vars c) v);
4.18 (*
4.19 val v = (term_of o the o (parse thy)) "x";
4.20 val t = (term_of o the o (parse thy)) "1";
4.21 @@ -328,11 +328,11 @@
4.22 let
4.23 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
4.24 val _=writeln("t= f@ts= \""^
4.25 - ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
4.26 - (commas(map(string_of_cterm o cterm_of (sign_of thy))ts))^"]\"");
4.27 + ((string_of_cterm o (Thm.cterm thy)) f)^"\" @ \"["^
4.28 + (commas(map(string_of_cterm o (Thm.cterm thy))ts))^"]\"");
4.29 val _=writeln("u= g@us= \""^
4.30 - ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
4.31 - (commas(map(string_of_cterm o cterm_of (sign_of thy))us))^"]\"");
4.32 + ((string_of_cterm o (Thm.cterm thy)) g)^"\" @ \"["^
4.33 + (commas(map(string_of_cterm o (Thm.cterm thy))us))^"]\"");
4.34 val _=writeln("size_of_term(t,u)= ("^
4.35 (string_of_int(size_of_term' t))^", "^
4.36 (string_of_int(size_of_term' u))^")");
4.37 @@ -453,10 +453,10 @@
4.38 (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
4.39 if is_polyexp arg
4.40 then SOME (mk_thmid thmid ""
4.41 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
4.42 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
4.43 Trueprop $ (mk_equality (t, HOLogic.true_const)))
4.44 else SOME (mk_thmid thmid ""
4.45 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
4.46 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
4.47 Trueprop $ (mk_equality (t, HOLogic.false_const)))
4.48 | eval_is_polyexp _ _ _ _ = NONE;
4.49
4.50 @@ -1186,10 +1186,10 @@
4.51 (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
4.52 if is_multUnordered arg
4.53 then SOME (mk_thmid thmid ""
4.54 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
4.55 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
4.56 Trueprop $ (mk_equality (t, HOLogic.true_const)))
4.57 else SOME (mk_thmid thmid ""
4.58 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
4.59 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
4.60 Trueprop $ (mk_equality (t, HOLogic.false_const)))
4.61 | eval_is_multUnordered _ _ _ _ = NONE;
4.62
4.63 @@ -1239,10 +1239,10 @@
4.64 (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
4.65 if is_addUnordered arg
4.66 then SOME (mk_thmid thmid ""
4.67 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
4.68 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
4.69 Trueprop $ (mk_equality (t, HOLogic.true_const)))
4.70 else SOME (mk_thmid thmid ""
4.71 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
4.72 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
4.73 Trueprop $ (mk_equality (t, HOLogic.false_const)))
4.74 | eval_is_addUnordered _ _ _ _ = NONE;
4.75
5.1 --- a/src/Tools/isac/IsacKnowledge/PolyEq.ML Fri Aug 20 12:25:37 2010 +0200
5.2 +++ b/src/Tools/isac/IsacKnowledge/PolyEq.ML Fri Aug 20 14:58:43 2010 +0200
5.3 @@ -1007,10 +1007,10 @@
5.4 let
5.5 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
5.6 val _=writeln("t= f@ts= \""^
5.7 - ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
5.8 + ((string_of_cterm o (Thm.cterm thy)) f)^"\" @ \"["^
5.9 (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
5.10 val _=writeln("u= g@us= \""^
5.11 - ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
5.12 + ((string_of_cterm o (Thm.cterm thy)) g)^"\" @ \"["^
5.13 (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
5.14 val _=writeln("size_of_term(t,u)= ("^
5.15 (string_of_int(size_of_term' x t))^", "^
6.1 --- a/src/Tools/isac/IsacKnowledge/RatEq.ML Fri Aug 20 12:25:37 2010 +0200
6.2 +++ b/src/Tools/isac/IsacKnowledge/RatEq.ML Fri Aug 20 14:58:43 2010 +0200
6.3 @@ -23,7 +23,7 @@
6.4 (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
6.5 fun is_rateqation_in t v =
6.6 let
6.7 - fun coeff_in c v = member op = v (vars c);
6.8 + fun coeff_in c v = member op = (vars c) v;
6.9 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:")
6.10 (* at the moment there is no term like this, but ....*)
6.11 | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v
7.1 --- a/src/Tools/isac/IsacKnowledge/Rational-WN.sml Fri Aug 20 12:25:37 2010 +0200
7.2 +++ b/src/Tools/isac/IsacKnowledge/Rational-WN.sml Fri Aug 20 14:58:43 2010 +0200
7.3 @@ -137,11 +137,11 @@
7.4 val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT;
7.5 val eT = HOLogic.realT;
7.6 val t = mk_mono cT vT pT eT ~5 "x" 5;
7.7 -cterm_of (sign_of thy) t;
7.8 +(Thm.cterm thy) t;
7.9 val t = mk_mono cT vT pT eT ~1 "x" 0;
7.10 -cterm_of (sign_of thy) t;
7.11 +(Thm.cterm thy) t;
7.12 val t = mk_mono cT vT pT eT 1 "x" 1;
7.13 -cterm_of (sign_of thy) t;
7.14 +(Thm.cterm thy) t;
7.15
7.16
7.17 fun mk_sum pT t1 t2 = Const ("op +", [pT, pT]--->pT) $ t1 $ t2;
7.18 @@ -164,21 +164,21 @@
7.19
7.20 (*tests*)
7.21 val t = poly2term cT vT pT eT [~1] "x";
7.22 -cterm_of (sign_of thy) t;
7.23 +(Thm.cterm thy) t;
7.24 val t = poly2term cT vT pT eT [0,1] "x";
7.25 -cterm_of (sign_of thy) t;
7.26 +(Thm.cterm thy) t;
7.27 val t = poly2term cT vT pT eT [0,0,0,1] "x";
7.28 -cterm_of (sign_of thy) t;
7.29 +(Thm.cterm thy) t;
7.30 val t = poly2term cT vT pT eT [0,0,0,3] "x";
7.31 -cterm_of (sign_of thy) t;
7.32 +(Thm.cterm thy) t;
7.33 val t = poly2term cT vT pT eT [~1,0,0,3] "x";
7.34 -cterm_of (sign_of thy) t;
7.35 +(Thm.cterm thy) t;
7.36 val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";
7.37 -cterm_of (sign_of thy) t;
7.38 +(Thm.cterm thy) t;
7.39 val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x";
7.40 -cterm_of (sign_of thy) t;
7.41 +(Thm.cterm thy) t;
7.42 val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x";
7.43 -cterm_of (sign_of thy) t;
7.44 +(Thm.cterm thy) t;
7.45
7.46 "***************************************************************************";
7.47 "* reverse-rewriting 12.8.02 *";
8.1 --- a/src/Tools/isac/IsacKnowledge/Rational.ML Fri Aug 20 12:25:37 2010 +0200
8.2 +++ b/src/Tools/isac/IsacKnowledge/Rational.ML Fri Aug 20 14:58:43 2010 +0200
8.3 @@ -2768,10 +2768,10 @@
8.4 (t as (Const("Rational.is'_expanded", _) $ arg)) thy =
8.5 if is_expanded arg
8.6 then SOME (mk_thmid thmid ""
8.7 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
8.8 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
8.9 Trueprop $ (mk_equality (t, HOLogic.true_const)))
8.10 else SOME (mk_thmid thmid ""
8.11 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
8.12 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
8.13 Trueprop $ (mk_equality (t, HOLogic.false_const)))
8.14 | eval_is_expanded _ _ _ _ = NONE;
8.15
8.16 @@ -3378,10 +3378,10 @@
8.17 (t as (Const("Rational.is'_ratpolyexp", _) $ arg)) thy =
8.18 if is_ratpolyexp arg
8.19 then SOME (mk_thmid thmid ""
8.20 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
8.21 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
8.22 Trueprop $ (mk_equality (t, HOLogic.true_const)))
8.23 else SOME (mk_thmid thmid ""
8.24 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
8.25 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
8.26 Trueprop $ (mk_equality (t, HOLogic.false_const)))
8.27 | eval_is_ratpolyexp _ _ _ _ = NONE;
8.28
9.1 --- a/src/Tools/isac/IsacKnowledge/Root.ML Fri Aug 20 12:25:37 2010 +0200
9.2 +++ b/src/Tools/isac/IsacKnowledge/Root.ML Fri Aug 20 14:58:43 2010 +0200
9.3 @@ -89,11 +89,11 @@
9.4 let
9.5 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
9.6 val _=writeln("t= f@ts= \""^
9.7 - ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
9.8 - (commas(map(string_of_cterm o cterm_of (sign_of thy)) ts))^"]\"");
9.9 + ((string_of_cterm o (Thm.cterm thy)) f)^"\" @ \"["^
9.10 + (commas(map(string_of_cterm o (Thm.cterm thy)) ts))^"]\"");
9.11 val _=writeln("u= g@us= \""^
9.12 - ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
9.13 - (commas(map(string_of_cterm o cterm_of (sign_of thy)) us))^"]\"");
9.14 + ((string_of_cterm o (Thm.cterm thy)) g)^"\" @ \"["^
9.15 + (commas(map(string_of_cterm o (Thm.cterm thy)) us))^"]\"");
9.16 val _=writeln("size_of_term(t,u)= ("^
9.17 (string_of_int(size_of_term' t))^", "^
9.18 (string_of_int(size_of_term' u))^")");
9.19 @@ -133,7 +133,7 @@
9.20
9.21 rew_ord' := overwritel (!rew_ord',
9.22 [("termlessI", termlessI),
9.23 - ("sqrt_right", sqrt_right false ProtoPure.thy)
9.24 + ("sqrt_right", sqrt_right false (theory "Pure"))
9.25 ]);
9.26
9.27 (*-------------------------rulse-------------------------*)
10.1 --- a/src/Tools/isac/IsacKnowledge/RootEq.ML Fri Aug 20 12:25:37 2010 +0200
10.2 +++ b/src/Tools/isac/IsacKnowledge/RootEq.ML Fri Aug 20 14:58:43 2010 +0200
10.3 @@ -23,7 +23,7 @@
10.4 (* true if bdv is under sqrt of a Equation*)
10.5 fun is_rootTerm_in t v =
10.6 let
10.7 - fun coeff_in c v = member op = v (vars c);
10.8 + fun coeff_in c v = member op = (vars c) v;
10.9 fun findroot (_ $ _ $ _ $ _) v = raise error("is_rootTerm_in:")
10.10 (* at the moment there is no term like this, but ....*)
10.11 | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v
10.12 @@ -37,7 +37,7 @@
10.13
10.14 fun is_sqrtTerm_in t v =
10.15 let
10.16 - fun coeff_in c v = member op = v (vars c);
10.17 + fun coeff_in c v = member op = (vars c) v;
10.18 fun findsqrt (_ $ _ $ _ $ _) v = raise error("is_sqrteqation_in:")
10.19 (* at the moment there is no term like this, but ....*)
10.20 | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v)
10.21 @@ -52,7 +52,7 @@
10.22 and the subterm ist connected with + or * --> is normalized*)
10.23 fun is_normSqrtTerm_in t v =
10.24 let
10.25 - fun coeff_in c v = member op = v (vars c);
10.26 + fun coeff_in c v = member op = (vars c) v;
10.27 fun isnorm (_ $ _ $ _ $ _) v = raise error("is_normSqrtTerm_in:")
10.28 (* at the moment there is no term like this, but ....*)
10.29 | isnorm (Const ("op +",_) $ _ $ t2) v = is_sqrtTerm_in t2 v
11.1 --- a/src/Tools/isac/IsacKnowledge/RootRatEq.ML Fri Aug 20 12:25:37 2010 +0200
11.2 +++ b/src/Tools/isac/IsacKnowledge/RootRatEq.ML Fri Aug 20 14:58:43 2010 +0200
11.3 @@ -26,7 +26,7 @@
11.4 if false then (term)^2 contains no (sq)root *)
11.5 fun is_rootRatAddTerm_in t v =
11.6 let
11.7 - fun coeff_in c v = member op = v (vars c);
11.8 + fun coeff_in c v = member op = (vars c) v;
11.9 fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse
11.10 (is_rootTerm_in t3 v)
11.11 | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse
12.1 --- a/src/Tools/isac/IsacKnowledge/Test.ML Fri Aug 20 12:25:37 2010 +0200
12.2 +++ b/src/Tools/isac/IsacKnowledge/Test.ML Fri Aug 20 14:58:43 2010 +0200
12.3 @@ -18,22 +18,22 @@
12.4 then raise error ("eval_root_free: wrong "^op0)
12.5 else if const_in (strip_thy op0) arg
12.6 then SOME (mk_thmid thmid ""
12.7 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
12.8 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
12.9 Trueprop $ (mk_equality (t, false_as_term)))
12.10 else SOME (mk_thmid thmid ""
12.11 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
12.12 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
12.13 Trueprop $ (mk_equality (t, true_as_term)))
12.14 | eval_root_free _ _ _ _ = NONE;
12.15
12.16 (*does a term contain a root ?*)
12.17 fun eval_contains_root (thmid:string) _
12.18 (t as (Const("Test.contains'_root",t0) $ arg)) thy =
12.19 - if member op = "sqrt" (ids_of arg)
12.20 + if member op = (ids_of arg) "sqrt"
12.21 then SOME (mk_thmid thmid ""
12.22 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
12.23 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
12.24 Trueprop $ (mk_equality (t, true_as_term)))
12.25 else SOME (mk_thmid thmid ""
12.26 - ((string_of_cterm o cterm_of (sign_of thy)) arg) "",
12.27 + ((string_of_cterm o (Thm.cterm thy)) arg) "",
12.28 Trueprop $ (mk_equality (t, false_as_term)))
12.29 | eval_contains_root _ _ _ _ = NONE;
12.30
12.31 @@ -84,7 +84,7 @@
12.32 (*FIXXXXXXME 10.8.02: handle like _simplify*)
12.33 val tval_rls =
12.34 Rls{id = "tval_rls", preconds = [],
12.35 - rew_ord = ("sqrt_right",sqrt_right false ProtoPure.thy),
12.36 + rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
12.37 erls=testerls,srls = e_rls,
12.38 calc=[],
12.39 rules = [Thm ("refl",num_str refl),
12.40 @@ -220,7 +220,7 @@
12.41 (* expects * distributed over + *)
12.42 val Test_simplify =
12.43 Rls{id = "Test_simplify", preconds = [],
12.44 - rew_ord = ("sqrt_right",sqrt_right false ProtoPure.thy),
12.45 + rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
12.46 erls = tval_rls, srls = e_rls,
12.47 calc=[(*since 040209 filled by prep_rls*)],
12.48 (*asm_thm = [],*)
12.49 @@ -633,7 +633,7 @@
12.50 \(matches (a + v_ ^^^2 = 0, e_::bool)) |\
12.51 \(matches ( v_ ^^^2 = 0, e_::bool))";
12.52 val prei = subst_atomic env pre;
12.53 - val cpre = cterm_of (sign_of thy) prei;
12.54 + val cpre = (Thm.cterm thy) prei;
12.55
12.56 val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;
12.57 val ct = "True | False | False | False" : cterm
12.58 @@ -1020,11 +1020,11 @@
12.59 let
12.60 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
12.61 val _=writeln("t= f@ts= \""^
12.62 - ((string_of_cterm o cterm_of (sign_of thy)) f)^"\" @ \"["^
12.63 - (commas(map(string_of_cterm o cterm_of (sign_of thy)) ts))^"]\"");
12.64 + ((string_of_cterm o (Thm.cterm thy)) f)^"\" @ \"["^
12.65 + (commas(map(string_of_cterm o (Thm.cterm thy)) ts))^"]\"");
12.66 val _=writeln("u= g@us= \""^
12.67 - ((string_of_cterm o cterm_of (sign_of thy)) g)^"\" @ \"["^
12.68 - (commas(map(string_of_cterm o cterm_of (sign_of thy)) us))^"]\"");
12.69 + ((string_of_cterm o (Thm.cterm thy)) g)^"\" @ \"["^
12.70 + (commas(map(string_of_cterm o (Thm.cterm thy)) us))^"]\"");
12.71 val _=writeln("size_of_term(t,u)= ("^
12.72 (string_of_int(size_of_term' t))^", "^
12.73 (string_of_int(size_of_term' u))^")");
13.1 --- a/src/Tools/isac/Isac_Mathengine.thy Fri Aug 20 12:25:37 2010 +0200
13.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Fri Aug 20 14:58:43 2010 +0200
13.3 @@ -36,20 +36,16 @@
13.4 use "ME/ctree.sml"
13.5 use "ME/ptyps.sml"
13.6 use "ME/generate.sml"
13.7 +use "ME/calchead.sml"
13.8
13.9
13.10 ML {*
13.11 +cterm_of;
13.12 111;
13.13 member op = [1,2,3] 2;
13.14 *}
13.15
13.16 -use "ME/calchead.sml"
13.17
13.18 -ML {*
13.19 -theory2theory';
13.20 -(assoc_thy "Script");
13.21 -(assoc_thy "Script.thy");
13.22 -*}
13.23
13.24 (*
13.25 use "ME/appl.sml"
14.1 --- a/src/Tools/isac/ME/appl.sml Fri Aug 20 12:25:37 2010 +0200
14.2 +++ b/src/Tools/isac/ME/appl.sml Fri Aug 20 14:58:43 2010 +0200
14.3 @@ -62,11 +62,11 @@
14.4 (*------------------------------------------------------------------*)
14.5
14.6 val op_and = Const ("op &", [bool, bool] ---> bool);
14.7 -(*> cterm_of (sign_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
14.8 +(*> (Thm.cterm thy) (op_and $ Free("a",bool) $ Free("b",bool));
14.9 val it = "a & b" : cterm
14.10 *)
14.11 fun mk_and a b = op_and $ a $ b;
14.12 -(*> cterm_of (sign_of thy)
14.13 +(*> (Thm.cterm thy)
14.14 (mk_and (Free("a",bool)) (Free("b",bool)));
14.15 val it = "a & b" : cterm*)
14.16
14.17 @@ -78,7 +78,7 @@
14.18 in mk t ts end;
14.19 (*> val pred = map (term_of o the o (parse thy))
14.20 ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
14.21 -> cterm_of (sign_of thy) (mk_and pred);
14.22 +> (Thm.cterm thy) (mk_and pred);
14.23 val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
14.24
14.25
14.26 @@ -180,7 +180,7 @@
14.27 > val pred = (term_of o the o (parse thy))
14.28 "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
14.29 > val ttt = check_elementwise thy consts (bdv, pred);
14.30 -> cterm_of (sign_of thy) ttt;
14.31 +> (Thm.cterm thy) ttt;
14.32 val it = "[x = #-3, x = #3]" : cterm
14.33
14.34 > val consts = (term_of o the o (parse thy)) "[x = #4]";
14.35 @@ -188,7 +188,7 @@
14.36 > val pred = (term_of o the o (parse thy))
14.37 "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
14.38 > val ttt = check_elementwise thy consts (bdv,pred);
14.39 -> cterm_of (sign_of thy) ttt;
14.40 +> (Thm.cterm thy) ttt;
14.41 val it = "[x = #4]" : cterm
14.42
14.43 > val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
14.44 @@ -196,7 +196,7 @@
14.45 > val pred = (term_of o the o (parse thy))
14.46 " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
14.47 > val ttt = check_elementwise thy consts (bdv,pred);
14.48 -> cterm_of (sign_of thy) ttt;
14.49 +> (Thm.cterm thy) ttt;
14.50 val it = "[]" : cterm*)
14.51
14.52
14.53 @@ -344,7 +344,7 @@
14.54 else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*)))
14.55
14.56 | applicable_in (p,p_) pt (Check_Postcond pI) =
14.57 - if member op = p_ [Pbl,Met]
14.58 + if member op = [Pbl,Met] p_
14.59 then Notappl ((tac2str (Check_Postcond pI))^
14.60 " not for pos "^(pos'2str (p,p_)))
14.61 else Appl (Check_Postcond'
14.62 @@ -358,7 +358,7 @@
14.63 (* val m as Rewrite_Inst (subs, thm') = m;
14.64 *)
14.65 | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) =
14.66 - if member op = p_ [Pbl,Met]
14.67 + if member op = [Pbl,Met] p_
14.68 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.69 else
14.70 let
14.71 @@ -389,7 +389,7 @@
14.72 val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac);
14.73 *)
14.74 | applicable_in (p,p_) pt (m as Rewrite thm') =
14.75 - if member op = p_ [Pbl,Met]
14.76 + if member op = [Pbl,Met] p_
14.77 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.78 else
14.79 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
14.80 @@ -413,7 +413,7 @@
14.81 end
14.82
14.83 | applicable_in (p,p_) pt (m as Rewrite_Asm thm') =
14.84 - if member op = p_ [Pbl,Met]
14.85 + if member op = [Pbl,Met] p_
14.86 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.87 else
14.88 let
14.89 @@ -435,7 +435,7 @@
14.90 | NONE => Notappl ("'"^(fst thm')^"' not applicable") end
14.91
14.92 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
14.93 - if member op = p_ [Pbl,Met]
14.94 + if member op = [Pbl,Met] p_
14.95 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.96 else
14.97 let
14.98 @@ -457,7 +457,7 @@
14.99 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
14.100
14.101 | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) =
14.102 - if member op = p_ [Pbl,Met]
14.103 + if member op = [Pbl,Met] p_
14.104 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.105 else
14.106 let
14.107 @@ -481,7 +481,7 @@
14.108 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
14.109
14.110 | applicable_in (p,p_) pt (m as Rewrite_Set rls) =
14.111 - if member op = p_ [Pbl,Met]
14.112 + if member op = [Pbl,Met] p_
14.113 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.114 else
14.115 let
14.116 @@ -500,7 +500,7 @@
14.117 | NONE => Notappl (rls^" not applicable") end
14.118
14.119 | applicable_in (p,p_) pt (m as Detail_Set rls) =
14.120 - if member op = p_ [Pbl,Met]
14.121 + if member op = [Pbl,Met] p_
14.122 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.123 else
14.124 let val pp = par_pblobj pt p
14.125 @@ -523,7 +523,7 @@
14.126 (* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);
14.127 *)
14.128 | applicable_in (p,p_) pt (m as Calculate op_) =
14.129 - if member op = p_ [Pbl,Met]
14.130 + if member op = [Pbl,Met] p_
14.131 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.132 else
14.133 let
14.134 @@ -544,7 +544,7 @@
14.135 (2) Pattern.match: for solving equational systems
14.136 (which raises exn for ?a..?z)*)
14.137 | applicable_in (p,p_) pt (m as Substitute sube) =
14.138 - if member op = p_ [Pbl,Met]
14.139 + if member op = [Pbl,Met] p_
14.140 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.141 else let val pp = par_pblobj pt p
14.142 val thy = assoc_thy (get_obj g_domID pt pp)
14.143 @@ -568,7 +568,7 @@
14.144 end
14.145 (*-------WN08114 interrupted with error in polyminus.sml "11 = 11"
14.146 | applicable_in (p,p_) pt (m as Substitute sube) =
14.147 - if member op = p_ [Pbl,Met]
14.148 + if member op = [Pbl,Met] p_
14.149 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.150 else let val pp = par_pblobj pt p
14.151 val thy = assoc_thy (get_obj g_domID pt pp)
14.152 @@ -589,7 +589,7 @@
14.153
14.154 (*'logical' applicability wrt. script in locate: Inconsistent?*)
14.155 | applicable_in (p,p_) pt (m as Take ct') =
14.156 - if member op = p_ [Pbl,Met]
14.157 + if member op = [Pbl,Met] p_
14.158 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.159 else
14.160 let val thy' = get_obj g_domID pt (par_pblobj pt p);
14.161 @@ -607,7 +607,7 @@
14.162 (tac2str (Group (con, ints))))
14.163
14.164 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
14.165 - if member op = p_ [Pbl,Met]
14.166 + if member op = [Pbl,Met] p_
14.167 then (*maybe Apply_Method has already been done*)
14.168 case get_obj g_env pt p of
14.169 SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [],
14.170 @@ -681,7 +681,7 @@
14.171 val ((p,p_), Check_elementwise pred) = (p, m);
14.172 *)
14.173 | applicable_in (p,p_) pt (m as Check_elementwise pred) =
14.174 - if member op = p_ [Pbl,Met]
14.175 + if member op = [Pbl,Met] p_
14.176 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
14.177 else
14.178 let
14.179 @@ -716,7 +716,7 @@
14.180 end
14.181
14.182 | applicable_in (p,p_) pt Or_to_List =
14.183 - if member op = p_ [Pbl,Met]
14.184 + if member op = [Pbl,Met] p_
14.185 then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
14.186 else
14.187 let
15.1 --- a/src/Tools/isac/ME/mathengine.sml Fri Aug 20 12:25:37 2010 +0200
15.2 +++ b/src/Tools/isac/ME/mathengine.sml Fri Aug 20 14:58:43 2010 +0200
15.3 @@ -121,7 +121,7 @@
15.4 | Appl m =>
15.5 (* val Appl m = applicable_in p pt m;
15.6 *)
15.7 - let val x = if member op = mI specsteps
15.8 + let val x = if member op = specsteps mI
15.9 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
15.10 in case x of
15.11 ERror e => ("failure", ([], [], ptp))
15.12 @@ -245,7 +245,7 @@
15.13 if ip = p (*the request is done where ptp waits for*)
15.14 then let val (pt',c',p') = generate tacis (pt,[],p)
15.15 in ("ok", (tacis, c', (pt', p'))) end
15.16 - else (case (if member op = p_ [Pbl,Met]
15.17 + else (case (if member op = [Pbl,Met] p_
15.18 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
15.19 handle _ => ([],[],ptp)(*e.g.by Add_Given "equality///"*)
15.20 of cs as ([],_,_) => ("helpless", cs)
15.21 @@ -256,11 +256,11 @@
15.22 NONE => ("no-fmz-spec", ([], [], ptp))
15.23 | SOME pI =>
15.24 (* val SOME pI = pIopt;
15.25 - val cs=(if member op = p_ [Pbl,Met] andalso is_none(get_obj g_env pt (fst p))
15.26 + val cs=(if member op = [Pbl,Met] p_ andalso is_none(get_obj g_env pt (fst p))
15.27 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
15.28 handle _ => ([], ptp);
15.29 *)
15.30 - (case (if member op = p_ [Pbl,Met]
15.31 + (case (if member op = [Pbl,Met] p_
15.32 andalso is_none (get_obj g_env pt (fst p))
15.33 (*^^^^^^^^: Apply_Method without init_form*)
15.34 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip) )
16.1 --- a/src/Tools/isac/ME/rewtools.sml Fri Aug 20 12:25:37 2010 +0200
16.2 +++ b/src/Tools/isac/ME/rewtools.sml Fri Aug 20 14:58:43 2010 +0200
16.3 @@ -244,7 +244,7 @@
16.4 (rule2str r1)^"' '"^(rule2str r2)^"'");
16.5 fun distinct_Thm r = gen_distinct eq_Thm r;
16.6
16.7 -fun eq_Thms thmIDs thm = (member op = (id_of_thm thm) thmIDs)
16.8 +fun eq_Thms thmIDs thm = (member op = thmIDs (id_of_thm thm))
16.9 handle _ => false;
16.10
16.11
16.12 @@ -721,7 +721,7 @@
16.13 let val guh' = explode guh
16.14 val part = implode (take_fromto 1 4 guh')
16.15 val isa = implode (take_fromto 5 9 guh')
16.16 - in if not (member op = part ["exp_", "thy_", "pbl_", "met_"])
16.17 + in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)
16.18 then raise error ("guh '"^guh^"' does not begin with \
16.19 \exp_ | thy_ | pbl_ | met_")
16.20 else let val chap = case isa of
17.1 --- a/src/Tools/isac/ME/script.sml Fri Aug 20 12:25:37 2010 +0200
17.2 +++ b/src/Tools/isac/ME/script.sml Fri Aug 20 14:58:43 2010 +0200
17.3 @@ -158,7 +158,7 @@
17.4 *)
17.5
17.6 fun test_negotiable t =
17.7 - member op = ((strip_thy o (term_str Script.thy) o head_of) t) (!negotiable);
17.8 + member op = (!negotiable) ((strip_thy o (term_str Script.thy) o head_of) t);
17.9
17.10 (*.get argument of first stactic in a script for init_form.*)
17.11 fun get_stac thy (h $ body) =
17.12 @@ -325,7 +325,7 @@
17.13 *)
17.14 fun itms2args thy mI (itms:itm list) =
17.15 let val mvat = max_vt itms
17.16 - fun okv mvat (_,vats,b,_,_) = member op = mvat vats andalso b
17.17 + fun okv mvat (_,vats,b,_,_) = member op = vats mvat andalso b
17.18 val itms = filter (okv mvat) itms
17.19 fun test_dsc d (_,_,_,_,itm_) = (d = d_in itm_)
17.20 fun itm2arg itms (_,(d,_)) =
17.21 @@ -509,7 +509,7 @@
17.22 > val asm = (term_of o the o (parse thy))
17.23 "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)";
17.24 > val pred = subst_atomic [s] asm;
17.25 -> rewrite_set_ thy false (cterm_of (sign_of thy) pred);
17.26 +> rewrite_set_ thy false ((Thm.cterm thy) pred);
17.27 val it = NONE : (cterm * cterm list) option !!!!!!!!!!!!!!!!!!!!!!!!!!!!
17.28 > eval_true' (string_of_thy thy) "eval_rls" (subst_atomic [s] pred);
17.29 val it = false : bool
17.30 @@ -519,7 +519,7 @@
17.31 > val asm = (term_of o the o (parse thy))
17.32 "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#5 + x)";
17.33 > val pred = subst_atomic [s] asm;
17.34 -> rewrite_set_ thy false (cterm_of (sign_of thy) pred);
17.35 +> rewrite_set_ thy false ((Thm.cterm thy) pred);
17.36 val it = SOME ("True & True",[]) : (cterm * cterm list) option
17.37 > eval_true' (string_of_thy thy) "eval_rls" (subst_atomic [s] pred);
17.38 val it = true : bool`*)
17.39 @@ -806,7 +806,7 @@
17.40 v
17.41 *)
17.42 fun make_rule thy t =
17.43 - let val ct = cterm_of (sign_of thy) (Trueprop $ t)
17.44 + let val ct = (Thm.cterm thy) (Trueprop $ t)
17.45 in Thm (string_of_cterm ct, make_thm ct) end;
17.46
17.47 (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
17.48 @@ -1918,7 +1918,7 @@
17.49 (* val (thy', (p,p_), pt) = (thy', (p,p_), pt);
17.50 *)
17.51 fun from_pblobj_or_detail' thy' (p,p_) pt =
17.52 - if member op = p_ [Pbl,Met]
17.53 + if member op = [Pbl,Met] p_
17.54 then case get_obj g_env pt p of
17.55 NONE => raise error "from_pblobj_or_detail': no istate"
17.56 | SOME is =>
18.1 --- a/src/Tools/isac/ME/solve.sml Fri Aug 20 12:25:37 2010 +0200
18.2 +++ b/src/Tools/isac/ME/solve.sml Fri Aug 20 14:58:43 2010 +0200
18.3 @@ -495,7 +495,7 @@
18.4 (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
18.5 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
18.6 if p = ([], Res) then ("end-of-calculation", [], ptp) else
18.7 - if member op = p_ [Pbl,Met]
18.8 + if member op = [Pbl,Met] p_
18.9 then let val ptp = all_modspec ptp
18.10 val (_, c', ptp) = all_solve auto c ptp
18.11 in complete_solve auto (c@c') ptp end
18.12 @@ -571,7 +571,7 @@
18.13 | Appl m =>
18.14 (* val Appl m=applicable_in (p,p_) pt m;
18.15 *)
18.16 - if member op = mI specsteps
18.17 + if member op = specsteps mI
18.18 then let val (_,_,f,_,_,_) = specify m (p,p_) [] pt
18.19 in f end
18.20 else let val (*_,_,f,_,_,_*)_ = solve (mI,m) (pt,(p,p_))
19.1 --- a/src/Tools/isac/Scripts/Tools.sml Fri Aug 20 12:25:37 2010 +0200
19.2 +++ b/src/Tools/isac/Scripts/Tools.sml Fri Aug 20 14:58:43 2010 +0200
19.3 @@ -46,7 +46,7 @@
19.4 \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\
19.5 \else hd [A = a * b, a // #2 = #2]";
19.6
19.7 -> cterm_of (sign_of thy) t';
19.8 +> (Thm.cterm thy) t';
19.9 > val t = (term_of o the o (parse thy)) s;
19.10 > val eval_fn = the (assoc (!eval_list, op_));
19.11 > val (SOME(_,t')) = get_pair op_ eval_fn t;
19.12 @@ -92,7 +92,7 @@
19.13
19.14 > val eval_fn = the (assoc (!eval_list, op_));
19.15 > val (SOME(id,t')) = get_pair op_ eval_fn t;
19.16 -> cterm_of (sign_of thy) t';
19.17 +> (Thm.cterm thy) t';
19.18 val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)"
19.19 *)
19.20
20.1 --- a/src/Tools/isac/Scripts/rewrite.sml Fri Aug 20 12:25:37 2010 +0200
20.2 +++ b/src/Tools/isac/Scripts/rewrite.sml Fri Aug 20 14:58:43 2010 +0200
20.3 @@ -405,7 +405,7 @@
20.4 (*prints subgoal etc.
20.5 ((goal thy);(topthm()) o ) str; *)
20.6 (*assume rejects scheme variables
20.7 - assume (cterm_of (sign_of thy) (Trueprop $
20.8 + assume ((Thm.cterm thy) (Trueprop $
20.9 (term_of o the o (parse thy)) str)); *)
20.10
20.11
21.1 --- a/src/Tools/isac/Scripts/term_G.sml Fri Aug 20 12:25:37 2010 +0200
21.2 +++ b/src/Tools/isac/Scripts/term_G.sml Fri Aug 20 14:58:43 2010 +0200
21.3 @@ -6,7 +6,7 @@
21.4 *)
21.5
21.6 (*
21.7 -> cterm_of (sign_of thy) a_term;
21.8 +> (Thm.cterm thy) a_term;
21.9 val it = "empty" : cterm *)
21.10
21.11 (*2003 fun match thy t pat =
21.12 @@ -261,7 +261,7 @@
21.13 > val tt = (term_of o the o (parse thy)) "R=(R::real)";
21.14 > val TT = type_of tt;
21.15 > val ss = list2isalist TT [tt,tt,tt];
21.16 -> cterm_of (sign_of thy) ss;
21.17 +> (Thm.cterm thy) ss;
21.18 val it = "[R = R, R = R, R = R]" : cterm *)
21.19
21.20 fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
21.21 @@ -574,7 +574,7 @@
21.22 (*
21.23 val T = (type_of o term_of o the) (parse thy "#12::real");
21.24 val t = mk_factroot "SqRoot.sqrt" T 2 3;
21.25 -cterm_of (sign_of thy) t;
21.26 +(Thm.cterm thy) t;
21.27 val it = "#2 * sqrt #3 " : cterm
21.28 *)
21.29 fun var_op_num v op_ optype ntyp n =
21.30 @@ -591,7 +591,7 @@
21.31 (*
21.32 > val t = num_op_num "Int" 3 4;
21.33 > atomty t;
21.34 -> string_of_cterm (cterm_of (sign_of thy) t);
21.35 +> string_of_cterm ((Thm.cterm thy) t);
21.36 *)
21.37
21.38 fun const_in str (Const _) = false
21.39 @@ -768,7 +768,7 @@
21.40 atomty t; (* 'a *)
21.41 val t' = set_types al t;
21.42 atomty t'; (*real*)
21.43 -cterm_of (sign_of thy) t';
21.44 +(Thm.cterm thy) t';
21.45 val it = "x = #0 + #-1 * #-4" : cterm
21.46
21.47 val t = (term_of o the o (parse thy))
21.48 @@ -776,7 +776,7 @@
21.49 atomty t;
21.50 val t' = set_types al t;
21.51 atomty t';
21.52 -cterm_of (sign_of thy) t';
21.53 +(Thm.cterm thy) t';
21.54 uncaught exception TYPE (*^^^ is new, NOT in al*)
21.55 *)
21.56
21.57 @@ -1110,7 +1110,7 @@
21.58 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
21.59 val t = Free ("R","?DUMMY") : term
21.60 > val t' = typ_a2real t;
21.61 -> cterm_of (sign_of thy) t';
21.62 +> (Thm.cterm thy) t';
21.63 val it = "R::RealDef.real" : cterm
21.64
21.65 > val str = "R=R";
21.66 @@ -1121,13 +1121,13 @@
21.67 *** Free ( R, RealDef.real)
21.68 *** Free ( R, RealDef.real)
21.69 > val t' = typ_a2real t;
21.70 -> cterm_of (sign_of thy) t';
21.71 +> (Thm.cterm thy) t';
21.72 val it = "(R::RealDef.real) = R" : cterm
21.73
21.74 > val str = "fixed_values [R=R]";
21.75 > val t = term_of (read_cterm(sign_of thy)(str,(TVar(("DUMMY",0),[]))));
21.76 > val t' = typ_a2real t;
21.77 -> cterm_of (sign_of thy) t';
21.78 +> (Thm.cterm thy) t';
21.79 val it = "fixed_values [(R::RealDef.real) = R]" : cterm
21.80 *)
21.81
22.1 --- a/test/Tools/isac/ME/inform.sml Fri Aug 20 12:25:37 2010 +0200
22.2 +++ b/test/Tools/isac/ME/inform.sml Fri Aug 20 14:58:43 2010 +0200
22.3 @@ -103,13 +103,13 @@
22.4 "----------------------------------------------------------";
22.5 val fod = make_deriv Isac.thy Atools_erls
22.6 ((#rules o rep_rls) Test_simplify)
22.7 - (sqrt_right false ProtoPure.thy) NONE
22.8 + (sqrt_right false (theory "Pure")) NONE
22.9 (str2term "x + 1 + -1 * 2 = 0");
22.10 (writeln o trtas2str) fod;
22.11
22.12 val ifod = make_deriv Isac.thy Atools_erls
22.13 ((#rules o rep_rls) Test_simplify)
22.14 - (sqrt_right false ProtoPure.thy) NONE
22.15 + (sqrt_right false (theory "Pure")) NONE
22.16 (str2term "-2 * 1 + (1 + x) = 0");
22.17 (writeln o trtas2str) ifod;
22.18 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2;