1.1 --- a/src/Tools/isac/Interpret/appl.sml Mon Dec 07 10:52:07 2015 +0100
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Mon Dec 07 11:25:02 2015 +0100
1.3 @@ -74,7 +74,7 @@
1.4 let fun mk t' (t::[]) = op_and $ t' $ t
1.5 | mk t' (t::ts) = mk (op_and $ t' $ t) ts
1.6 in mk t ts end;
1.7 -(*> val pred = map (term_of o the o (parse thy))
1.8 +(*> val pred = map (Thm.term_of o the o (parse thy))
1.9 ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
1.10 > (Thm.global_cterm_of thy) (mk_and pred);
1.11 val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
1.12 @@ -90,7 +90,7 @@
1.13 then [pred]
1.14 else get_assumptions_ pt (p,Res))
1.15
1.16 -(* val pred = (term_of o the o (parse thy)) pred;
1.17 +(* val pred = (Thm.term_of o the o (parse thy)) pred;
1.18 val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;
1.19 mk_set thy pt p consts pred;
1.20 *)
1.21 @@ -168,29 +168,29 @@
1.22 val ct' = "HOL.True" : cterm'
1.23
1.24
1.25 -> val const = (term_of o the o (parse thy)) "(#3::real)";
1.26 +> val const = (Thm.term_of o the o (parse thy)) "(#3::real)";
1.27 > val pred' = subst_atomic [(bdv,const)] pred;
1.28
1.29
1.30 -> val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]";
1.31 -> val bdv = (term_of o the o (parse thy)) "(x::real)";
1.32 -> val pred = (term_of o the o (parse thy))
1.33 +> val consts = (Thm.term_of o the o (parse thy)) "[x = #-3, x = #3]";
1.34 +> val bdv = (Thm.term_of o the o (parse thy)) "(x::real)";
1.35 +> val pred = (Thm.term_of o the o (parse thy))
1.36 "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
1.37 > val ttt = check_elementwise thy consts (bdv, pred);
1.38 > (Thm.global_cterm_of thy) ttt;
1.39 val it = "[x = #-3, x = #3]" : cterm
1.40
1.41 -> val consts = (term_of o the o (parse thy)) "[x = #4]";
1.42 -> val bdv = (term_of o the o (parse thy)) "(x::real)";
1.43 -> val pred = (term_of o the o (parse thy))
1.44 +> val consts = (Thm.term_of o the o (parse thy)) "[x = #4]";
1.45 +> val bdv = (Thm.term_of o the o (parse thy)) "(x::real)";
1.46 +> val pred = (Thm.term_of o the o (parse thy))
1.47 "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
1.48 > val ttt = check_elementwise thy consts (bdv,pred);
1.49 > (Thm.global_cterm_of thy) ttt;
1.50 val it = "[x = #4]" : cterm
1.51
1.52 -> val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
1.53 -> val bdv = (term_of o the o (parse thy)) "(x::real)";
1.54 -> val pred = (term_of o the o (parse thy))
1.55 +> val consts = (Thm.term_of o the o (parse thy)) "[x = #-12 // #5]";
1.56 +> val bdv = (Thm.term_of o the o (parse thy)) "(x::real)";
1.57 +> val pred = (Thm.term_of o the o (parse thy))
1.58 " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
1.59 > val ttt = check_elementwise thy consts (bdv,pred);
1.60 > (Thm.global_cterm_of thy) ttt;
1.61 @@ -706,7 +706,7 @@
1.62 ^f);*)
1.63 val (id',f') = split_dummy (term2str f);
1.64 (*val _= tracing("### applicable_in: f'= "^f');*)
1.65 - (*val _= (term_of o the o (parse thy)) f';*)
1.66 + (*val _= (Thm.term_of o the o (parse thy)) f';*)
1.67 (*val _= tracing"### applicable_in: solve_equation_dummy";*)
1.68 in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
1.69 else if (thy2ctxt thy, f') |-> parseNEW |> the |> is_expliceq
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Dec 07 10:52:07 2015 +0100
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Dec 07 11:25:02 2015 +0100
2.3 @@ -243,7 +243,7 @@
2.4 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
2.5
2.6 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)
2.7 -fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f
2.8 +fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (Thm.term_of o the o (parse thy)) f
2.9 | f_mout thy _ = error "f_mout: not called with formula";
2.10
2.11
2.12 @@ -271,9 +271,9 @@
2.13 | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);
2.14 (*
2.15 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
2.16 -> val (_,t1) = split_dsc_t hs (term_of ct);
2.17 +> val (_,t1) = split_dsc_t hs (Thm.term_of ct);
2.18 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
2.19 -> val (_,t2) = split_dsc_t hs (term_of ct);
2.20 +> val (_,t2) = split_dsc_t hs (Thm.term_of ct);
2.21 > typeless t1 = typeless t2;
2.22 val it = true : bool
2.23 *)
2.24 @@ -388,10 +388,10 @@
2.25 | has_list_type _ = false;
2.26 (*
2.27 > val (SOME ct) = parse thy "lll::real list";
2.28 -> has_list_type (term_of ct);
2.29 +> has_list_type (Thm.term_of ct);
2.30 val it = true : bool
2.31 > val (SOME ct) = parse thy "[lll::real]";
2.32 -> has_list_type (term_of ct);
2.33 +> has_list_type (Thm.term_of ct);
2.34 val it = false : bool *)
2.35
2.36 fun is_parsed (Syn _) = false
2.37 @@ -1533,7 +1533,7 @@
2.38
2.39
2.40 (*fun tag_form thy (formal, given) = Thm.global_cterm_of thy
2.41 - (((head_of o term_of) given) $ (term_of formal)); WN100819*)
2.42 + (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819*)
2.43 fun tag_form thy (formal, given) =
2.44 (let
2.45 val gf = (head_of given) $ formal;
2.46 @@ -1557,11 +1557,11 @@
2.47 find the failing item:
2.48 > val n = 2;
2.49 > val tag__form = chktyp (n,formals,givens);
2.50 -> (type_of o term_of o (nth n)) formals;
2.51 -> (type_of o term_of o (nth n)) givens;
2.52 -> atomty ((term_of o (nth n)) formals);
2.53 -> atomty ((term_of o (nth n)) givens);
2.54 -> atomty (term_of tag__form);
2.55 +> (type_of o Thm.term_of o (nth n)) formals;
2.56 +> (type_of o Thm.term_of o (nth n)) givens;
2.57 +> atomty ((Thm.term_of o (nth n)) formals);
2.58 +> atomty ((Thm.term_of o (nth n)) givens);
2.59 +> atomty (Thm.term_of tag__form);
2.60 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";
2.61 ##################################################### *)
2.62
2.63 @@ -1582,14 +1582,14 @@
2.64 val givens = map (the o (parse thy)) given;
2.65
2.66 val tag__forms = chktyps (formals, givens);
2.67 -map ((atomty) o term_of) tag__forms;
2.68 +map ((atomty) o Thm.term_of) tag__forms;
2.69 ##################################################### *)
2.70
2.71
2.72 (* check pbltypes, announces one failure a time *)
2.73 (*fun chk_vars ctppc =
2.74 let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} =
2.75 - appc flat (mappc (vars o term_of) ctppc)
2.76 + appc flat (mappc (vars o Thm.term_of) ctppc)
2.77 in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)
2.78 else if (re\\(gi union fi)) <> []
2.79 then ("re\\(gi union fi)",re\\(gi union fi))
2.80 @@ -1632,8 +1632,8 @@
2.81 in ((fld f) o rev) xs end;
2.82 (*
2.83 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
2.84 -> val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
2.85 -> val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
2.86 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
2.87 +> val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
2.88 > Thm.global_cterm_of thy conj;
2.89 val it = "(a = b & c = d) & e = f" : cterm
2.90 *)
2.91 @@ -1644,8 +1644,8 @@
2.92 | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
2.93 (*
2.94 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
2.95 -> val ces = map (Thm.global_cterm_of thy) (isalist2list (term_of ct));
2.96 -> val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
2.97 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
2.98 +> val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
2.99 > Thm.global_cterm_of thy conj;
2.100 val it = "a = b & c = d & e = f & g = h" : cterm
2.101 *)
3.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Dec 07 10:52:07 2015 +0100
3.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Dec 07 11:25:02 2015 +0100
3.3 @@ -187,11 +187,11 @@
3.4 in itm end
3.5 handle _ => ((i,v,false,f, Syn (term2str t)):itm))
3.6 | parsitm dI (itm as (i,v,b,f, Syn str)) =
3.7 - (let val t = (term_of o the o (parse dI)) str
3.8 + (let val t = (Thm.term_of o the o (parse dI)) str
3.9 in (i,v,b,f, Par str) end
3.10 handle _ => (i,v,b,f, Syn str))
3.11 | parsitm dI (itm as (i,v,b,f, Typ str)) =
3.12 - (let val t = (term_of o the o (parse dI)) str
3.13 + (let val t = (Thm.term_of o the o (parse dI)) str
3.14 in (i,v,b,f, Par str) end
3.15 handle _ => (i,v,b,f, Syn str))
3.16 | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
3.17 @@ -263,7 +263,7 @@
3.18 | SOME ct =>
3.19 (* val SOME ct = parse thy str;
3.20 *)
3.21 - let val (d,ts) = (split_dts o term_of) ct
3.22 + let val (d,ts) = (split_dts o Thm.term_of) ct
3.23 val popt = find_first (eq7 (f,d)) pbt
3.24 in case popt of
3.25 NONE => ([1](*??*), true(*??*), f, Sup (d,ts))
3.26 @@ -663,7 +663,7 @@
3.27 case parse (assoc_thy "Isac") istr of
3.28 SOME f_in =>
3.29 let
3.30 - val f_in = term_of f_in
3.31 + val f_in = Thm.term_of f_in
3.32 val f_succ = get_curr_formula (pt, pos);
3.33 in
3.34 if f_succ = f_in
4.1 --- a/src/Tools/isac/Interpret/mstools.sml Mon Dec 07 10:52:07 2015 +0100
4.2 +++ b/src/Tools/isac/Interpret/mstools.sml Mon Dec 07 11:25:02 2015 +0100
4.3 @@ -270,20 +270,20 @@
4.4 "solutions L"
4.5
4.6 before 6.5.03:
4.7 -> val t = (term_of o the o (parse thy)) "testdscforlist [#1]";
4.8 +> val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]";
4.9 > val (d,ts) = split_dts t;
4.10 > comp_dts thy (d,ts);
4.11 val it = "testdscforlist [#1]" : cterm
4.12
4.13 -> val t = (term_of o the o (parse thy)) "(A::real)";
4.14 +> val t = (Thm.term_of o the o (parse thy)) "(A::real)";
4.15 > val (d,ts) = split_dts t;
4.16 val d = Const ("empty","empty") : term
4.17 val ts = [Free ("A","RealDef.real")] : term list
4.18 -> val t = (term_of o the o (parse thy)) "[R=(R::real)]";
4.19 +> val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]";
4.20 > val (d,ts) = split_dts t;
4.21 val d = Const ("empty","empty") : term
4.22 val ts = [Const # $ Free # $ Free (#,#)] : term list
4.23 -> val t = (term_of o the o (parse thy)) "[#1,#2]";
4.24 +> val t = (Thm.term_of o the o (parse thy)) "[#1,#2]";
4.25 > val (d,ts) = split_dts t;
4.26 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
4.27 *)
4.28 @@ -408,13 +408,13 @@
4.29 Const ("Script.Arbfix",_) => (id, v2)
4.30 | _ => (id, v1));
4.31 (*
4.32 - val e_ = (term_of o the o (parse thy)) "e_::bool";
4.33 - val ev = (term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0";
4.34 - val v_ = (term_of o the o (parse thy)) "v_";
4.35 - val vv = (term_of o the o (parse thy)) "x";
4.36 - val r_ = (term_of o the o (parse thy)) "err_::bool";
4.37 - val rv1 = (term_of o the o (parse thy)) "#0";
4.38 - val rv2 = (term_of o the o (parse thy)) "eps";
4.39 + val e_ = (Thm.term_of o the o (parse thy)) "e_::bool";
4.40 + val ev = (Thm.term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0";
4.41 + val v_ = (Thm.term_of o the o (parse thy)) "v_";
4.42 + val vv = (Thm.term_of o the o (parse thy)) "x";
4.43 + val r_ = (Thm.term_of o the o (parse thy)) "err_::bool";
4.44 + val rv1 = (Thm.term_of o the o (parse thy)) "#0";
4.45 + val rv2 = (Thm.term_of o the o (parse thy)) "eps";
4.46
4.47 val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv;
4.48 map getval penv;
4.49 @@ -610,7 +610,7 @@
4.50 val t as t1 $ t2 = str2term "antiDerivativeName M_b";
4.51 pbl_ids ctxt t1 t2;
4.52
4.53 - val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
4.54 + val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
4.55 val (d,argl) = strip_comb t;
4.56 is_dsc d; (*see split_dts*)
4.57 dest_list (d,argl);
4.58 @@ -620,17 +620,17 @@
4.59 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
4.60 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
4.61
4.62 - val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x";
4.63 + val (dsc,vl) = (split_dts o Thm.term_of o the o (parse thy)) "solveFor x";
4.64 val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term
4.65 val vl = Free ("x","RealDef.real") : term
4.66
4.67 - val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
4.68 + val (dsc,id) = (split_did o Thm.term_of o the o (parse thy)) "solveFor v_";
4.69 pbl_ids ctxt dsc vl;
4.70 val it = [Free ("x","RealDef.real")] : term list
4.71
4.72 - val (dsc,vl) = (split_dts o term_of o the o(parse thy))
4.73 + val (dsc,vl) = (split_dts o Thm.term_of o the o(parse thy))
4.74 "errorBound (eps=#0)";
4.75 - val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";
4.76 + val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_";
4.77 pbl_ids ctxt dsc vl;
4.78 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *)
4.79
4.80 @@ -667,15 +667,15 @@
4.81 );
4.82 (*
4.83 val penv = [];
4.84 - val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x";
4.85 - val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";
4.86 + val (dsc,vl) = (split_did o Thm.term_of o the o (parse thy)) "solveFor x";
4.87 + val (dsc,id) = (split_did o Thm.term_of o the o (parse thy)) "solveFor v_";
4.88 val penv = upd_penv thy penv dsc (id, vl);
4.89 [(Free ("v_","RealDef.real"),
4.90 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])]
4.91 : (term * term list) list
4.92
4.93 - val (dsc,vl) = (split_did o term_of o the o(parse thy))"errorBound (eps=#0)";
4.94 - val (dsc,id) = (split_did o term_of o the o(parse thy))"errorBound err_";
4.95 + val (dsc,vl) = (split_did o Thm.term_of o the o(parse thy))"errorBound (eps=#0)";
4.96 + val (dsc,id) = (split_did o Thm.term_of o the o(parse thy))"errorBound err_";
4.97 upd_penv thy penv dsc (id, vl);
4.98 [(Free ("v_","RealDef.real"),
4.99 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]),
4.100 @@ -694,8 +694,8 @@
4.101 (*
4.102 val i = 2;
4.103 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
4.104 - val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
4.105 - val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
4.106 + val (dsc,vl) = (split_did o Thm.term_of o the o(parse thy))"boundVariable b";
4.107 + val (dsc,id) = (split_did o Thm.term_of o the o(parse thy))"boundVariable v_";
4.108 upd thy envv dsc (id, vl) i;
4.109 val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])
4.110 : int * (term * term list) list*)
4.111 @@ -715,15 +715,15 @@
4.112 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;
4.113
4.114 val vats = [2]
4.115 - val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";
4.116 - val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";
4.117 + val (dsc,vl) = (split_did o Thm.term_of o the o(parse thy))"boundVariable b";
4.118 + val (dsc,id) = (split_did o Thm.term_of o the o(parse thy))"boundVariable v_";
4.119 val envv = upd_envv thy envv vats dsc id vl;
4.120 val envv = [(2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])]
4.121 : (int * (term * term list) list) list
4.122
4.123 val vats = [1,2,3];
4.124 - val (dsc,vl) = (split_did o term_of o the o(parse thy))"maximum A";
4.125 - val (dsc,id) = (split_did o term_of o the o(parse thy))"maximum m_";
4.126 + val (dsc,vl) = (split_did o Thm.term_of o the o(parse thy))"maximum A";
4.127 + val (dsc,id) = (split_did o Thm.term_of o the o(parse thy))"maximum m_";
4.128 upd_envv thy envv vats dsc id vl;
4.129 [(1,[(Free ("m_","bool"),[Free ("A","bool")])]),
4.130 (2,
4.131 @@ -734,9 +734,9 @@
4.132
4.133
4.134 val env = []:envv;
4.135 - val (d,ts) = (split_dts o term_of o the o (parse thy))
4.136 + val (d,ts) = (split_dts o Thm.term_of o the o (parse thy))
4.137 "fixedValues [r=Arbfix]";
4.138 - val (_,id) = (split_did o term_of o the o (parse thy))"fixedValues fix_";
4.139 + val (_,id) = (split_did o Thm.term_of o the o (parse thy))"fixedValues fix_";
4.140 val vats = [1,2,3];
4.141 val env = upd_envv thy env vats d id (mkval ts);
4.142 *)
4.143 @@ -904,7 +904,7 @@
4.144 | ts_in (Mis _) = [];
4.145 (*WN050629 unused*)
4.146 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
4.147 -val unique = (term_of o the o (parse (Thy_Info.get_theory "Real"))) "UnIqE_tErM";
4.148 +val unique = (Thm.term_of o the o (parse (Thy_Info.get_theory "Real"))) "UnIqE_tErM";
4.149 fun d_in (Cor ((d,_),_)) = d
4.150 | d_in (Syn (c)) = (tracing("*** d_in: Syn ("^c^")"); unique)
4.151 | d_in (Typ (c)) = (tracing("*** d_in: Typ ("^c^")"); unique)
5.1 --- a/src/Tools/isac/Interpret/ptyps.sml Mon Dec 07 10:52:07 2015 +0100
5.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Mon Dec 07 11:25:02 2015 +0100
5.3 @@ -7,7 +7,7 @@
5.4 *)
5.5
5.6 (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*)
5.7 -val dsc_unknown = (term_of o the o (parseold @{theory Script}))
5.8 +val dsc_unknown = (Thm.term_of o the o (parseold @{theory Script}))
5.9 "unknown::'a => unknow";
5.10 (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*)
5.11
5.12 @@ -92,11 +92,11 @@
5.13 end)
5.14 handle _ => error ("split_dsc: called with " ^ term2str t);
5.15 (*
5.16 -> val t1 = (term_of o the o (parse thy)) "errorBound err_";
5.17 +> val t1 = (Thm.term_of o the o (parse thy)) "errorBound err_";
5.18 > split_dsc t1;
5.19 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool"))
5.20 : term * term
5.21 -> val t3 = (term_of o the o (parse thy)) "valuesFor vs_";
5.22 +> val t3 = (Thm.term_of o the o (parse thy)) "valuesFor vs_";
5.23 > split_dsc t3;
5.24 (Const ("Descript.valuesFor","bool List.list => Tools.toreall"),
5.25 Free ("vs_","bool List.list")) : term * term*)
5.26 @@ -389,7 +389,7 @@
5.27 val gi = (case gi of
5.28 [] => []
5.29 | ((_,gi')::[]) =>
5.30 - ((map (split_did o term_of o the o (parse thy)) gi')
5.31 + ((map (split_did o Thm.term_of o the o (parse thy)) gi')
5.32 handle _ => error
5.33 ("prep_pbt: syntax error in '#Given' of "^
5.34 (strs2str pblID)))
5.35 @@ -415,7 +415,7 @@
5.36 (* val ((_,fi')::[]) = fi;
5.37 *)
5.38 | ((_,fi')::[]) =>
5.39 - ((map (split_did o term_of o the o (parse thy)) fi')
5.40 + ((map (split_did o Thm.term_of o the o (parse thy)) fi')
5.41 handle _ => error
5.42 ("prep_pbt: syntax error in '#Find' of "^
5.43 (strs2str pblID)))
5.44 @@ -428,7 +428,7 @@
5.45 val re = (case re of
5.46 [] => []
5.47 | ((_,re')::[]) =>
5.48 - ((map (split_did o term_of o the o (parse thy)) re')
5.49 + ((map (split_did o Thm.term_of o the o (parse thy)) re')
5.50 handle _ => error
5.51 ("prep_pbt: syntax error in '#Relate' of "^
5.52 (strs2str pblID)))
5.53 @@ -451,7 +451,7 @@
5.54 in ({guh=guh,mathauthors=maa,init=init,
5.55 thy=thy,cas= case ca of NONE => NONE
5.56 | SOME s =>
5.57 - SOME ((term_of o the o (parse thy)) s),
5.58 + SOME ((Thm.term_of o the o (parse thy)) s),
5.59 prls=ev,where_=wh,ppc= gi @ fi @ re,
5.60 met=metIDs}, pblID):pbt * pblID end;
5.61 (* prep_pbt thy (pblID, dsc_dats, metIDs);
5.62 @@ -479,7 +479,7 @@
5.63 val gi = (case gi of
5.64 [] => (writeln ("prep_met: in " ^ guh ^ " #Given is empty ?!?"); [])
5.65 | ((_,gi')::[]) =>
5.66 - ((map (split_did o term_of o the o (parse thy)) gi')
5.67 + ((map (split_did o Thm.term_of o the o (parse thy)) gi')
5.68 handle _ => error
5.69 ("prep_pbt: syntax error in '#Given' of "^
5.70 (strs2str metID)))
5.71 @@ -492,7 +492,7 @@
5.72 val fi = (case fi of
5.73 [] => (writeln ("prep_met: in " ^ guh ^ " #Find is empty ?!?"); [])
5.74 | ((_,fi')::[]) =>
5.75 - ((map (split_did o term_of o the o (parse thy)) fi')
5.76 + ((map (split_did o Thm.term_of o the o (parse thy)) fi')
5.77 handle _ => error
5.78 ("prep_pbt: syntax error in '#Find' of "^
5.79 (strs2str metID)))
5.80 @@ -505,7 +505,7 @@
5.81 val re = (case re of
5.82 [] => (writeln ("prep_met: in " ^ guh ^ " #Relate is empty ?!?"); [])
5.83 | ((_,re')::[]) =>
5.84 - ((map (split_did o term_of o the o (parse thy)) re')
5.85 + ((map (split_did o Thm.term_of o the o (parse thy)) re')
5.86 handle _ => error
5.87 ("prep_pbt: syntax error in '#Relate' of "^
5.88 (strs2str metID)))
5.89 @@ -525,7 +525,7 @@
5.90 | _ =>
5.91 (error ("prep_pbt: more than one '#Where' in "^
5.92 (strs2str metID))));
5.93 - val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr)
5.94 + val sc = (((inst_abs thy) o Thm.term_of o the o (parse thy)) scr)
5.95 in ({guh=guh,mathauthors=maa,init=init,
5.96 ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,
5.97 calc = if scr = "empty_script" then []
6.1 --- a/src/Tools/isac/Interpret/script.sml Mon Dec 07 10:52:07 2015 +0100
6.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Dec 07 11:25:02 2015 +0100
6.3 @@ -115,14 +115,14 @@
6.4 | go (R::p) (t1 $ t2) = go p t2
6.5 | go l _ = error ("go: no "^(loc_2str l));
6.6 (*
6.7 -> val t = (term_of o the o (parse thy)) "a+b";
6.8 +> val t = (Thm.term_of o the o (parse thy)) "a+b";
6.9 val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
6.10 > val plus_a = go [L] t;
6.11 > val b = go [R] t;
6.12 > val plus = go [L,L] t;
6.13 > val a = go [L,R] t;
6.14
6.15 -> val t = (term_of o the o (parse thy)) "a+b+c";
6.16 +> val t = (Thm.term_of o the o (parse thy)) "a+b+c";
6.17 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
6.18 > val pl_pl_a_b = go [L] t;
6.19 > val c = go [R] t;
6.20 @@ -148,7 +148,7 @@
6.21 NONE => get (l@[R]) test t2
6.22 | SOME (l',t') => SOME (l',t');
6.23 (*18.6.00
6.24 -> val sss = ((term_of o the o (parse thy))
6.25 +> val sss = ((Thm.term_of o the o (parse thy))
6.26 "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
6.27 \ (let e_ = Try (Rewrite square_equation_left True eq_) \
6.28 \ in [e_])");
6.29 @@ -225,10 +225,10 @@
6.30 | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term
6.31 | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
6.32 | itr_arg thy t = error ("itr_arg not impl. for " ^ term_to_string'' thy t);
6.33 -(* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
6.34 +(* val t = (Thm.term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
6.35 > itr_arg "Script" t;
6.36 val it = Free ("e_","RealDef.real") : term
6.37 -> val t = (term_of o the o (parse thy))"xxx";
6.38 +> val t = (Thm.term_of o the o (parse thy))"xxx";
6.39 > itr_arg "Script" t;
6.40 *** itr_arg not impl. for xxx
6.41 uncaught exception ERROR
6.42 @@ -261,13 +261,13 @@
6.43
6.44 (*get the _result_-type of a description*)
6.45 fun dsc_valT (Const (_,(Type (_,[_,T])))) = (strip_thy o typ_str) T;
6.46 -(*> val t = (term_of o the o (parse thy)) "equality";
6.47 +(*> val t = (Thm.term_of o the o (parse thy)) "equality";
6.48 > val T = type_of t;
6.49 val T = "bool => Tools.una" : typ
6.50 > val dsc = dsc_valT t;
6.51 val dsc = "una" : string
6.52
6.53 -> val t = (term_of o the o (parse thy)) "fixedValues";
6.54 +> val t = (Thm.term_of o the o (parse thy)) "fixedValues";
6.55 > val T = type_of t;
6.56 val T = "bool List.list => Tools.nam" : typ
6.57 > val dsc = dsc_valT t;
6.58 @@ -330,7 +330,7 @@
6.59
6.60 (*detour necessary, because generate1 delivers a string-result*)
6.61 fun mout2term thy (Form' (FormKF (_,_,_,_,res))) =
6.62 - (term_of o the o (parse (assoc_thy thy))) res
6.63 + (Thm.term_of o the o (parse (assoc_thy thy))) res
6.64 | mout2term thy (Form' (PpcKF _)) = e_term;(*3.8.01: res of subpbl
6.65 at time of detection in script*)
6.66
6.67 @@ -426,10 +426,10 @@
6.68 fun list_of_consts (Const ("List.list.Cons",_) $ _ $ _) = true
6.69 | list_of_consts (Const ("List.list.Nil",_)) = true
6.70 | list_of_consts _ = false;
6.71 -(*val ttt = (term_of o the o (parse thy)) "[x=#1,x=#2,x=#3]";
6.72 +(*val ttt = (Thm.term_of o the o (parse thy)) "[x=#1,x=#2,x=#3]";
6.73 > list_of_consts ttt;
6.74 val it = true : bool
6.75 -> val ttt = (term_of o the o (parse thy)) "[]";
6.76 +> val ttt = (Thm.term_of o the o (parse thy)) "[]";
6.77 > list_of_consts ttt;
6.78 val it = true : bool*)
6.79
6.80 @@ -579,7 +579,7 @@
6.81
6.82 | assod pt _ (m as Tac_ (thy,f,id,f')) (Const ("Script.Tac",_) $ Free (id',_)) =
6.83 if id = id'
6.84 - then Ass (m, ((term_of o the o (parse thy)) f'))
6.85 + then Ass (m, ((Thm.term_of o the o (parse thy)) f'))
6.86 else NotAss
6.87
6.88 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
6.89 @@ -676,14 +676,14 @@
6.90 unly needed --- **)
6.91
6.92 val idT = Type ("Script.ID",[]);
6.93 -(*val tt = (term_of o the o (parse thy)) "square_equation_left::ID";
6.94 +(*val tt = (Thm.term_of o the o (parse thy)) "square_equation_left::ID";
6.95 type_of tt = idT;
6.96 val it = true : bool
6.97 *)
6.98
6.99 fun make_rule thy t =
6.100 let val ct = Thm.global_cterm_of thy (Trueprop $ t)
6.101 - in Thm (term_to_string''' thy (term_of ct), Thm.make_thm ct) end;
6.102 + in Thm (term_to_string''' thy (Thm.term_of ct), Thm.make_thm ct) end;
6.103
6.104 (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
6.105 *)
6.106 @@ -709,7 +709,7 @@
6.107 val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
6.108 ML> subs;
6.109 val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
6.110 -> val tt = (term_of o the o (parse thy))
6.111 +> val tt = (Thm.term_of o the o (parse thy))
6.112 "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
6.113 > atomty tt;
6.114 ML> tracing (term2str tt);
6.115 @@ -722,14 +722,14 @@
6.116
6.117
6.118 (*Fehlersuche 1-2Monate vor 4.01:*)
6.119 -> val tt = (term_of o the o (parse thy))
6.120 +> val tt = (Thm.term_of o the o (parse thy))
6.121 "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";
6.122 > atomty tt;
6.123
6.124 -> val f = (term_of o the o (parse thy)) "x=#1+#2";
6.125 -> val f' = (term_of o the o (parse thy)) "x=#3";
6.126 -> val subs = [((term_of o the o (parse thy)) "bdv",
6.127 - (term_of o the o (parse thy)) "x")];
6.128 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
6.129 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
6.130 +> val subs = [((Thm.term_of o the o (parse thy)) "bdv",
6.131 + (Thm.term_of o the o (parse thy)) "x")];
6.132 > val sT = (type_of o fst o hd) subs;
6.133 > val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
6.134 (map HOLogic.mk_prod subs);
6.135 @@ -750,11 +750,11 @@
6.136 $ Free (thmID,idT) $ b $ f;
6.137 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
6.138 (*
6.139 -> val tt = (term_of o the o (parse thy)) (*____ ____..test*)
6.140 +> val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
6.141 "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";
6.142
6.143 -> val f = (term_of o the o (parse thy)) "x=#1+#2";
6.144 -> val f' = (term_of o the o (parse thy)) "x=#3";
6.145 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
6.146 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
6.147 > val Thm (id,thm) =
6.148 rep_tac_ (Rewrite'
6.149 ("Script","tless_true","eval_rls",false,
6.150 @@ -796,12 +796,12 @@
6.151 val t = HOLogic.mk_eq (lhs,f');
6.152 make_rule thy t;
6.153 --------------------------------------------------
6.154 -val lll = (term_of o the o (parse thy))
6.155 +val lll = (Thm.term_of o the o (parse thy))
6.156 "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
6.157
6.158 --------------------------------------------------
6.159 -> val f = (term_of o the o (parse thy)) "x=#1+#2";
6.160 -> val f' = (term_of o the o (parse thy)) "x=#3";
6.161 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
6.162 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
6.163 > val Thm (id,thm) =
6.164 rep_tac_ (Rewrite_Set'
6.165 ("Script",false,"SqRoot_simplify",f,(f',[])));
6.166 @@ -814,7 +814,7 @@
6.167 $ Free (op_,idT) $ f
6.168 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
6.169 (*
6.170 -> val lhs'=(term_of o the o (parse thy))"Calculate plus (#1+#2)";
6.171 +> val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";
6.172 ... test-root-equ.sml: calculate ...
6.173 > val Appl m'=applicable_in p pt (Calculate "PLUS");
6.174 > val (lhs,_)=tac_2etac m';
7.1 --- a/src/Tools/isac/Interpret/solve.sml Mon Dec 07 10:52:07 2015 +0100
7.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Dec 07 11:25:02 2015 +0100
7.3 @@ -117,8 +117,8 @@
7.4 (* use"ME/solve.sml";
7.5 use"solve.sml";
7.6
7.7 -val ttt = (term_of o the o (parse thy))"Substitute [(bdv,x)] g";
7.8 -val ttt = (term_of o the o (parse thy))"Rewrite thmid True g";
7.9 +val ttt = (Thm.term_of o the o (parse thy))"Substitute [(bdv,x)] g";
7.10 +val ttt = (Thm.term_of o the o (parse thy))"Rewrite thmid True g";
7.11
7.12 Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thm',_) $ Const (pa,_) $ f'
7.13 *)
8.1 --- a/src/Tools/isac/Knowledge/Atools.thy Mon Dec 07 10:52:07 2015 +0100
8.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Mon Dec 07 11:25:02 2015 +0100
8.3 @@ -663,7 +663,7 @@
8.4 Calc ("Atools.occurs'_in",eval_occurs_in ""),
8.5 Calc ("Tools.matches",eval_matches "")
8.6 ],
8.7 - scr = Prog ((term_of o the o (parse @{theory})) "empty_script")
8.8 + scr = Prog ((Thm.term_of o the o (parse @{theory})) "empty_script")
8.9 }:rls);
8.10 *)
8.11 "******* Atools.ML end *******";
9.1 --- a/src/Tools/isac/Knowledge/Diff.thy Mon Dec 07 10:52:07 2015 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Dec 07 11:25:02 2015 +0100
9.3 @@ -273,10 +273,10 @@
9.4 val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
9.5 *)
9.6 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
9.7 - [((term_of o the o (parse thy)) "functionTerm", [t]),
9.8 - ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
9.9 - ((term_of o the o (parse thy)) "derivative",
9.10 - [(term_of o the o (parse thy)) "f_f'"])
9.11 + [((Thm.term_of o the o (parse thy)) "functionTerm", [t]),
9.12 + ((Thm.term_of o the o (parse thy)) "differentiateFor", [bdv]),
9.13 + ((Thm.term_of o the o (parse thy)) "derivative",
9.14 + [(Thm.term_of o the o (parse thy)) "f_f'"])
9.15 ]
9.16 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
9.17 *}
9.18 @@ -386,7 +386,7 @@
9.19 " (Try (Rewrite_Set norm_Rational False))) f_f')")]
9.20 *}
9.21 setup {* KEStore_Elems.add_cas
9.22 - [((term_of o the o (parse thy)) "Diff",
9.23 + [((Thm.term_of o the o (parse thy)) "Diff",
9.24 (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss))] *}
9.25 ML {*
9.26
9.27 @@ -395,15 +395,15 @@
9.28 val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
9.29 *)
9.30 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
9.31 - [((term_of o the o (parse thy)) "functionEq", [t]),
9.32 - ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
9.33 - ((term_of o the o (parse thy)) "derivativeEq",
9.34 - [(term_of o the o (parse thy)) "f_f'::bool"])
9.35 + [((Thm.term_of o the o (parse thy)) "functionEq", [t]),
9.36 + ((Thm.term_of o the o (parse thy)) "differentiateFor", [bdv]),
9.37 + ((Thm.term_of o the o (parse thy)) "derivativeEq",
9.38 + [(Thm.term_of o the o (parse thy)) "f_f'::bool"])
9.39 ]
9.40 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
9.41 *}
9.42 setup {* KEStore_Elems.add_cas
9.43 - [((term_of o the o (parse thy)) "Differentiate",
9.44 + [((Thm.term_of o the o (parse thy)) "Differentiate",
9.45 (("Isac", ["named","derivative_of","function"], ["no_met"]), argl2dtss))] *}
9.46
9.47 end
10.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Mon Dec 07 10:52:07 2015 +0100
10.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldpbl.sml Mon Dec 07 11:25:02 2015 +0100
10.3 @@ -330,7 +330,7 @@
10.4 (*
10.5 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
10.6 val (SOME ct) = parse thy ;
10.7 -atomty thy (term_of ct);
10.8 +atomty thy (Thm.term_of ct);
10.9 *)
10.10
10.11
10.12 @@ -365,5 +365,5 @@
10.13 (*
10.14 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
10.15 val (SOME ct) = parse thy ;
10.16 -atomty thy (term_of ct);
10.17 +atomty thy (Thm.term_of ct);
10.18 *)
11.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Mon Dec 07 10:52:07 2015 +0100
11.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Mon Dec 07 11:25:02 2015 +0100
11.3 @@ -141,7 +141,7 @@
11.4 (*
11.5 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
11.6 val (SOME ct) = parse thy ;
11.7 -atomty (term_of ct);
11.8 +atomty (Thm.term_of ct);
11.9 *)
11.10
11.11
11.12 @@ -211,14 +211,14 @@
11.13 "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
11.14 "{R::real}"];
11.15 val tag__forms = chktyps thy (formals, givens);
11.16 -map ((atomty) o term_of) tag__forms;
11.17 +map ((atomty) o Thm.term_of) tag__forms;
11.18
11.19 val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
11.20 "alpha::real","{alpha. #0<alpha & alpha<pi//#2}",
11.21 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
11.22 "{R::real}"];
11.23 val tag__forms = chktyps thy (formals, givens);
11.24 -map ((atomty) o term_of) tag__forms;
11.25 +map ((atomty) o Thm.term_of) tag__forms;
11.26 *)
11.27
11.28 " --- subproblem: make-function-by-subst --- ";
11.29 @@ -236,7 +236,7 @@
11.30 val givens = map (the o (parse thy)) given;
11.31 (* 5.3.00
11.32 val tag__forms = chktyps thy (formals, givens);
11.33 -map ((atomty) o term_of) tag__forms;
11.34 +map ((atomty) o Thm.term_of) tag__forms;
11.35 *)
11.36 " --- subproblem: max-of-function --- ";
11.37 val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \
11.38 @@ -255,7 +255,7 @@
11.39 val givens = map (the o (parse thy)) given;
11.40 (* 5.3.00
11.41 val tag__forms = chktyps thy (formals, givens);
11.42 -map ((atomty) o term_of) tag__forms;
11.43 +map ((atomty) o Thm.term_of) tag__forms;
11.44 *)
11.45 " --- subproblem: derivative --- ";
11.46 val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10","x::real"];
11.47 @@ -270,7 +270,7 @@
11.48 val givens = map (the o (parse thy)) given;
11.49 (*
11.50 val tag__forms = chktyps thy (formals, givens);
11.51 -map ((atomty) o term_of) tag__forms;
11.52 +map ((atomty) o Thm.term_of) tag__forms;
11.53 *)
11.54 " --- subproblem: tan-quadrat-equation --- ";
11.55 val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \
11.56 @@ -289,7 +289,7 @@
11.57 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
11.58 val givens = map (the o (parse thy)) given;
11.59 val tag__forms = chktyps thy (formals, givens);
11.60 -map ((atomty) o term_of) tag__forms;
11.61 +map ((atomty) o Thm.term_of) tag__forms;
11.62 *)
11.63 (* use"test-coil-kernel.sml";
11.64 *)
12.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Mon Dec 07 10:52:07 2015 +0100
12.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Mon Dec 07 11:25:02 2015 +0100
12.3 @@ -72,7 +72,7 @@
12.4 Calc ("Atools.is'_const", eval_const "#is_const_"),
12.5 Calc ("Atools.occurs'_in", eval_occurs_in ""),
12.6 Calc ("Tools.matches", eval_matches "")],
12.7 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
12.8 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
12.9 }:rls);
12.10 *}
12.11 setup {* KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))] *}
13.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Dec 07 10:52:07 2015 +0100
13.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Dec 07 11:25:02 2015 +0100
13.3 @@ -213,7 +213,7 @@
13.4 (*Rls_ add_fractions_p, #2*)
13.5 Rls_ cancel_p
13.6 ],
13.7 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
13.8 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
13.9 }:rls;
13.10 *}
13.11 ML {*
13.12 @@ -234,7 +234,7 @@
13.13 Rls_ add_fractions_p,
13.14 Rls_ cancel_p
13.15 ],
13.16 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
13.17 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
13.18 }:rls;
13.19 *}
13.20 ML {*
14.1 --- a/src/Tools/isac/Knowledge/Equation.thy Mon Dec 07 10:52:07 2015 +0100
14.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Mon Dec 07 11:25:02 2015 +0100
14.3 @@ -67,7 +67,7 @@
14.4 (*.function for handling the cas-input "solve (x+1=2, x)":
14.5 make a model which is already in ptree-internal format.*)
14.6 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
14.7 - val (h,argl) = strip_comb ((term_of o the o (parse thy))
14.8 + val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy))
14.9 "solveTest (x+1=2, x)");
14.10 *)
14.11 fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
14.12 @@ -79,9 +79,9 @@
14.13 | argl2dtss _ = error "Equation.ML: wrong argument for argl2dtss";
14.14 *}
14.15 setup {* KEStore_Elems.add_cas
14.16 - [((term_of o the o (parse thy)) "solveTest",
14.17 + [((Thm.term_of o the o (parse thy)) "solveTest",
14.18 (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),
14.19 - ((term_of o the o (parse thy)) "solve",
14.20 + ((Thm.term_of o the o (parse thy)) "solve",
14.21 (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]*}
14.22
14.23
15.1 --- a/src/Tools/isac/Knowledge/InsSort.sml Mon Dec 07 10:52:07 2015 +0100
15.2 +++ b/src/Tools/isac/Knowledge/InsSort.sml Mon Dec 07 11:25:02 2015 +0100
15.3 @@ -33,7 +33,7 @@
15.4 Thm ("if_True", if_True),
15.5 Thm ("if_False", if_False)
15.6 ],
15.7 - scr = Prog ((term_of o the o (parse thy))
15.8 + scr = Prog ((Thm.term_of o the o (parse thy))
15.9 "empty_script")
15.10 }:rls;
15.11
15.12 @@ -63,7 +63,7 @@
15.13 ],
15.14 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
15.15 scr = Prog (((inst_abs (assoc_thm "InsSort"))
15.16 - o term_of o the o (parse thy)) (*for [#1,#3,#2] only*)
15.17 + o Thm.term_of o the o (parse thy)) (*for [#1,#3,#2] only*)
15.18 "Script Ins_sort (u_::'a list) = \
15.19 \ (let u_ = Rewrite sort_def False u_; \
15.20 \ u_ = Rewrite foldr_rec False u_; \
15.21 @@ -90,7 +90,7 @@
15.22 ("#Find" ,"sorted s_")
15.23 ],
15.24 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
15.25 - scr = Prog ((inst_abs o term_of o the o (parse thy))
15.26 + scr = Prog ((inst_abs o Thm.term_of o the o (parse thy))
15.27 "Script Sort (u_::'a list) = \
15.28 \ Rewrite_Set ins_sort False u_")
15.29 } : met)
16.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Dec 07 10:52:07 2015 +0100
16.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Dec 07 11:25:02 2015 +0100
16.3 @@ -202,13 +202,13 @@
16.4 Thm ("rat_power", num_str @{thm rat_power})
16.5 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
16.6 ],
16.7 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.8 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
16.9 }),
16.10 Rls_ make_rat_poly_with_parentheses,
16.11 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
16.12 Rls_ rat_reduce_1
16.13 ],
16.14 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.15 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
16.16 }:rls;
16.17
16.18 (*.for simplify_Integral adapted from 'norm_Rational'.*)
16.19 @@ -223,7 +223,7 @@
16.20 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
16.21 Rls_ discard_parentheses1 (* mult only *)
16.22 ],
16.23 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.24 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
16.25 }:rls;
16.26
16.27 (*.simplify terms before and after Integration such that
17.1 --- a/src/Tools/isac/Knowledge/Poly.thy Mon Dec 07 10:52:07 2015 +0100
17.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Dec 07 11:25:02 2015 +0100
17.3 @@ -197,14 +197,14 @@
17.4 (*.a 'c is coefficient of v' if v does NOT occur in c.*)
17.5 fun coeff_in c v = not (member op = (vars c) v);
17.6 (* FIXME.WN100826 shift this into test--------------
17.7 - val v = (term_of o the o (parse thy)) "x";
17.8 - val t = (term_of o the o (parse thy)) "1";
17.9 + val v = (Thm.term_of o the o (parse thy)) "x";
17.10 + val t = (Thm.term_of o the o (parse thy)) "1";
17.11 coeff_in t v;
17.12 (*val it = true : bool*)
17.13 - val t = (term_of o the o (parse thy)) "a*b+c";
17.14 + val t = (Thm.term_of o the o (parse thy)) "a*b+c";
17.15 coeff_in t v;
17.16 (*val it = true : bool*)
17.17 - val t = (term_of o the o (parse thy)) "a*x+c";
17.18 + val t = (Thm.term_of o the o (parse thy)) "a*x+c";
17.19 coeff_in t v;
17.20 (*val it = false : bool*)
17.21 ----------------------------------------------------*)
17.22 @@ -226,26 +226,26 @@
17.23 if coeff_in m v then (*case 1*) SOME 0
17.24 else factor_right_deg m v;
17.25 (* FIXME.WN100826 shift this into test-----------------------------
17.26 - val v = (term_of o the o (parse thy)) "x";
17.27 - val t = (term_of o the o (parse thy)) "(a*b+c)*x^^^7";
17.28 + val v = (Thm.term_of o the o (parse thy)) "x";
17.29 + val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";
17.30 mono_deg_in t v;
17.31 (*val it = SOME 7*)
17.32 - val t = (term_of o the o (parse thy)) "x^^^7";
17.33 + val t = (Thm.term_of o the o (parse thy)) "x^^^7";
17.34 mono_deg_in t v;
17.35 (*val it = SOME 7*)
17.36 - val t = (term_of o the o (parse thy)) "(a*b+c)*x";
17.37 + val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";
17.38 mono_deg_in t v;
17.39 (*val it = SOME 1*)
17.40 - val t = (term_of o the o (parse thy)) "(a*b+x)*x";
17.41 + val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";
17.42 mono_deg_in t v;
17.43 (*val it = NONE*)
17.44 - val t = (term_of o the o (parse thy)) "x";
17.45 + val t = (Thm.term_of o the o (parse thy)) "x";
17.46 mono_deg_in t v;
17.47 (*val it = SOME 1*)
17.48 - val t = (term_of o the o (parse thy)) "(a*b+c)";
17.49 + val t = (Thm.term_of o the o (parse thy)) "(a*b+c)";
17.50 mono_deg_in t v;
17.51 (*val it = SOME 0*)
17.52 - val t = (term_of o the o (parse thy)) "ab - (a*b)*x";
17.53 + val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";
17.54 mono_deg_in t v;
17.55 (*val it = NONE*)
17.56 ------------------------------------------------------------------*)
17.57 @@ -280,20 +280,20 @@
17.58 | NONE => NONE)
17.59 in edi ~1 ~1 t end;
17.60 (* FIXME.WN100826 shift this into test-----------------------------
17.61 - val v = (term_of o the o (parse thy)) "x";
17.62 - val t = (term_of o the o (parse thy)) "a+b";
17.63 + val v = (Thm.term_of o the o (parse thy)) "x";
17.64 + val t = (Thm.term_of o the o (parse thy)) "a+b";
17.65 expand_deg_in t v;
17.66 (*val it = SOME 0*)
17.67 - val t = (term_of o the o (parse thy)) "(a+b)*x";
17.68 + val t = (Thm.term_of o the o (parse thy)) "(a+b)*x";
17.69 expand_deg_in t v;
17.70 (*SOME 1*)
17.71 - val t = (term_of o the o (parse thy)) "a*b - (a+b)*x";
17.72 + val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x";
17.73 expand_deg_in t v;
17.74 (*SOME 1*)
17.75 - val t = (term_of o the o (parse thy)) "a*b + (a-b)*x";
17.76 + val t = (Thm.term_of o the o (parse thy)) "a*b + (a-b)*x";
17.77 expand_deg_in t v;
17.78 (*SOME 1*)
17.79 - val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
17.80 + val t = (Thm.term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
17.81 expand_deg_in t v;
17.82 -------------------------------------------------------------------*)
17.83 fun poly_deg_in t v =
17.84 @@ -326,14 +326,14 @@
17.85 case expand_deg_in t v of SOME d => d | NONE => ~1;
17.86 end;(*local*)
17.87 (* FIXME.WN100826 shift this into test-----------------------------
17.88 - val v = (term_of o the o (parse thy)) "x";
17.89 - val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
17.90 + val v = (Thm.term_of o the o (parse thy)) "x";
17.91 + val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
17.92 has_degree_in t v;
17.93 (*val it = 2*)
17.94 - val t = (term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
17.95 + val t = (Thm.term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
17.96 has_degree_in t v;
17.97 (*val it = 2*)
17.98 - val t = (term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";
17.99 + val t = (Thm.term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";
17.100 has_degree_in t v;
17.101 (*val it = 2*)
17.102 -------------------------------------------------------------------*)
17.103 @@ -348,7 +348,7 @@
17.104 Trueprop $ (mk_equality (p, @{term False})))
17.105 | eval_is_expanded_in _ _ _ _ = NONE;
17.106 (*
17.107 - val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
17.108 + val t = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
17.109 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
17.110 (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
17.111 term2str t';
17.112 @@ -365,7 +365,7 @@
17.113 Trueprop $ (mk_equality (p, @{term False})))
17.114 | eval_is_poly_in _ _ _ _ = NONE;
17.115 (*
17.116 - val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
17.117 + val t = (Thm.term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
17.118 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
17.119 (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
17.120 term2str t';
17.121 @@ -382,7 +382,7 @@
17.122 end
17.123 | eval_has_degree_in _ _ _ _ = NONE;
17.124 (*
17.125 -> val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
17.126 +> val t = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
17.127 > val SOME (id, t') = eval_has_degree_in 0 0 t 0;
17.128 val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
17.129 > term2str t';
17.130 @@ -1100,7 +1100,7 @@
17.131 Calc ("Groups.times_class.times", eval_binop "#mult_"),
17.132 Calc ("Atools.pow", eval_binop "#power_")
17.133 ],
17.134 - scr = Prog ((term_of o the o (parse thy)) scr_expand_binoms)
17.135 + scr = Prog ((Thm.term_of o the o (parse thy)) scr_expand_binoms)
17.136 }:rls;
17.137
17.138
18.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Dec 07 10:52:07 2015 +0100
18.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Dec 07 11:25:02 2015 +0100
18.3 @@ -450,7 +450,7 @@
18.4 Thm ("cancel_leading_coeff11",num_str @{thm cancel_leading_coeff11}),
18.5 Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),
18.6 Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
18.7 - ],scr = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);
18.8 + ],scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")}:rls);
18.9
18.10 val prep_rls' = prep_rls @{theory};
18.11 *}
18.12 @@ -465,7 +465,7 @@
18.13 Thm ("complete_square4",num_str @{thm complete_square4}),
18.14 Thm ("complete_square5",num_str @{thm complete_square5})
18.15 ],
18.16 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.17 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.18 }:rls);
18.19
18.20 val polyeq_simplify = prep_rls'(
18.21 @@ -487,7 +487,7 @@
18.22 Calc ("Atools.pow" ,eval_binop "#power_"),
18.23 Rls_ reduce_012
18.24 ],
18.25 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.26 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.27 }:rls);
18.28 *}
18.29 setup {* KEStore_Elems.add_rlss
18.30 @@ -509,7 +509,7 @@
18.31 rules = [Thm("d0_true",num_str @{thm d0_true}),
18.32 Thm("d0_false",num_str @{thm d0_false})
18.33 ],
18.34 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.35 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.36 }:rls);
18.37
18.38 (* -- d1 -- *)
18.39 @@ -528,7 +528,7 @@
18.40 Thm("d1_isolate_div",num_str @{thm d1_isolate_div})
18.41 (* bx=c -> x=c/b *)
18.42 ],
18.43 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.44 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.45 }:rls);
18.46
18.47 *}
18.48 @@ -551,7 +551,7 @@
18.49 Thm ("d2_reduce_equation2", num_str @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 |a+ x=0*)
18.50 Thm ("d2_isolate_div", num_str @{thm d2_isolate_div}) (* bx^2=c -> x^2=c/b *)
18.51 ],
18.52 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.53 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.54 }:rls);
18.55 *}
18.56 ML{*
18.57 @@ -578,7 +578,7 @@
18.58 Thm("d2_isolate_div",num_str @{thm d2_isolate_div})
18.59 (* bx^2=c -> x^2=c/b*)
18.60 ],
18.61 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.62 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.63 }:rls);
18.64 *}
18.65 ML{*
18.66 @@ -624,7 +624,7 @@
18.67 (* x^2=0 *)
18.68 Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
18.69 (* 1x^2=0 *)
18.70 - ],scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.71 + ],scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.72 }:rls);
18.73 *}
18.74 ML{*
18.75 @@ -671,7 +671,7 @@
18.76 Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
18.77 (* bx^2=0 *)
18.78 ],
18.79 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.80 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.81 }:rls);
18.82 *}
18.83 ML{*
18.84 @@ -731,7 +731,7 @@
18.85 Thm("d2_isolate_div",num_str @{thm d2_isolate_div})
18.86 (* bx^2=c -> x^2=c/b*)
18.87 ],
18.88 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.89 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.90 }:rls);
18.91 *}
18.92 ML{*
18.93 @@ -804,7 +804,7 @@
18.94 Thm("d3_root_equation1",num_str @{thm d3_root_equation1})
18.95 (*bdv^^^3=c) = (bdv = nroot 3 c*)
18.96 ],
18.97 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.98 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.99 }:rls);
18.100 *}
18.101 ML{*
18.102 @@ -819,7 +819,7 @@
18.103 [Thm("d4_sub_u1",num_str @{thm d4_sub_u1})
18.104 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
18.105 ],
18.106 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.107 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
18.108 }:rls);
18.109 *}
18.110 setup {* KEStore_Elems.add_rlss
19.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Mon Dec 07 10:52:07 2015 +0100
19.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Mon Dec 07 11:25:02 2015 +0100
19.3 @@ -143,7 +143,7 @@
19.4 Thm("rat_mult_denominator_right",num_str @{thm rat_mult_denominator_right})
19.5 (* a/b=c -> a=cb *)
19.6 ],
19.7 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
19.8 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
19.9 }:rls);
19.10 *}
19.11 setup {* KEStore_Elems.add_rlss [("RatEq_eliminate",
19.12 @@ -171,7 +171,7 @@
19.13 Thm("rat_double_rat_3",num_str @{thm rat_double_rat_3})
19.14 (* ((a/b) / c = a / (b*c) ) *)
19.15 ],
19.16 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
19.17 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
19.18 }:rls);
19.19 *}
19.20 setup {* KEStore_Elems.add_rlss [("RatEq_simplify",
20.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Mon Dec 07 10:52:07 2015 +0100
20.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Mon Dec 07 11:25:02 2015 +0100
20.3 @@ -2,16 +2,16 @@
20.4
20.5 (*protokoll 14.3.02 --------------------------------------------------
20.6 val ct = parse thy "(a + #1)//(#2*a^^^#2 - #2)";
20.7 -val t = (term_of o the) ct;
20.8 +val t = (Thm.term_of o the) ct;
20.9 atomt t;
20.10 val ct = parse thy "not (#1+a)"; (*HOL.thy ?*)
20.11 -val t = (term_of o the) ct;
20.12 +val t = (Thm.term_of o the) ct;
20.13 atomt t;
20.14 val ct = parse thy "x"; (*momentan ist alles 'real'*)
20.15 -val t = (term_of o the) ct;
20.16 +val t = (Thm.term_of o the) ct;
20.17 atomty t;
20.18 val ct = parse thy "(x::int)"; (* !!! *)
20.19 -val t = (term_of o the) ct;
20.20 +val t = (Thm.term_of o the) ct;
20.21 atomty t;
20.22
20.23 val ct = parse thy "(x::int)*(y::real)"; (*momentan ist alles 'real'*)
20.24 @@ -79,27 +79,27 @@
20.25 SOME (poly t v 0) handle _ => NONE;
20.26
20.27 (*tests*)
20.28 -val v = (term_of o the o (parse thy)) "x::real";
20.29 -val t = (term_of o the o (parse thy)) "#-1::real";
20.30 +val v = (Thm.term_of o the o (parse thy)) "x::real";
20.31 +val t = (Thm.term_of o the o (parse thy)) "#-1::real";
20.32 term2poly t v;
20.33 -val t = (term_of o the o (parse thy)) "x::real";
20.34 +val t = (Thm.term_of o the o (parse thy)) "x::real";
20.35 term2poly t v;
20.36 -val t = (term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*)
20.37 +val t = (Thm.term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*)
20.38 term2poly t v;
20.39 -val t = (term_of o the o (parse thy)) "x^^^#1"; (*FIXME: drop it*)
20.40 +val t = (Thm.term_of o the o (parse thy)) "x^^^#1"; (*FIXME: drop it*)
20.41 term2poly t v;
20.42 -val t = (term_of o the o (parse thy)) "x^^^#3";
20.43 +val t = (Thm.term_of o the o (parse thy)) "x^^^#3";
20.44 term2poly t v;
20.45 -val t = (term_of o the o (parse thy)) "#3 * x^^^#3";
20.46 +val t = (Thm.term_of o the o (parse thy)) "#3 * x^^^#3";
20.47 term2poly t v;
20.48 -val t = (term_of o the o (parse thy)) "#-1 + #3 * x^^^#3";
20.49 +val t = (Thm.term_of o the o (parse thy)) "#-1 + #3 * x^^^#3";
20.50 term2poly t v;
20.51 -val t = (term_of o the o (parse thy)) "#-1 + (#3 * x^^^#3 + #5 * x^^^#5)";
20.52 +val t = (Thm.term_of o the o (parse thy)) "#-1 + (#3 * x^^^#3 + #5 * x^^^#5)";
20.53 term2poly t v;
20.54 -val t = (term_of o the o (parse thy))
20.55 +val t = (Thm.term_of o the o (parse thy))
20.56 "#-1 + (#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7))";
20.57 term2poly t v;
20.58 -val t = (term_of o the o (parse thy))
20.59 +val t = (Thm.term_of o the o (parse thy))
20.60 "#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7)";
20.61 term2poly t v;
20.62
21.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Dec 07 10:52:07 2015 +0100
21.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Dec 07 11:25:02 2015 +0100
21.3 @@ -194,7 +194,7 @@
21.4 end
21.5
21.6 fun term_of_poly baseT expT vs p =
21.7 - let val monos = map (term_of_monom baseT expT vs) p
21.8 + let val monos = map (Thm.term_of_monom baseT expT vs) p
21.9 in foldl (HOLogic.mk_binop "Groups.plus_class.plus") (hd monos, tl monos) end
21.10 *}
21.11
21.12 @@ -245,7 +245,7 @@
21.13 val t' =
21.14 HOLogic.mk_binop "Fields.inverse_class.divide"
21.15 (HOLogic.mk_binop "Groups.times_class.times"
21.16 - (term_of_poly baseT expT vs a', ct),
21.17 + (Thm.term_of_poly baseT expT vs a', ct),
21.18 HOLogic.mk_binop "Groups.times_class.times" (b't, ct))
21.19 in SOME (t', mk_asms baseT [b't, ct]) end
21.20 end
21.21 @@ -290,7 +290,7 @@
21.22 val ct = term_of_poly baseT expT vs c
21.23 val t' =
21.24 HOLogic.mk_binop "Fields.inverse_class.divide"
21.25 - (term_of_poly baseT expT vs a', bt')
21.26 + (Thm.term_of_poly baseT expT vs a', bt')
21.27 val asm = mk_asms baseT [bt']
21.28 in SOME (t', asm) end
21.29 end
21.30 @@ -336,7 +336,7 @@
21.31 let
21.32 val ((a', b'), c) = gcd_poly a b
21.33 val (baseT, expT) = (type_of n1, HOLogic.realT)
21.34 - val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
21.35 + val [d1', d2', c'] = map (Thm.term_of_poly baseT expT vs) [a', b', c]
21.36 (*----- minimum of parentheses & nice result, but breaks tests: -------------
21.37 val denom = HOLogic.mk_binop "Groups.times_class.times"
21.38 (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*)
22.1 --- a/src/Tools/isac/Knowledge/Root.thy Mon Dec 07 10:52:07 2015 +0100
22.2 +++ b/src/Tools/isac/Knowledge/Root.thy Mon Dec 07 11:25:02 2015 +0100
22.3 @@ -250,7 +250,7 @@
22.4 Calc ("Groups.times_class.times", eval_binop "#mult_"),
22.5 Calc ("Atools.pow", eval_binop "#power_")
22.6 ],
22.7 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
22.8 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
22.9 }:rls);
22.10 *}
22.11 setup {* KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))] *}
22.12 @@ -324,7 +324,7 @@
22.13 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
22.14 Calc ("Atools.pow", eval_binop "#power_")
22.15 ],
22.16 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
22.17 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
22.18 }:rls);
22.19 *}
22.20 setup {* KEStore_Elems.add_rlss
23.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Dec 07 10:52:07 2015 +0100
23.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon Dec 07 11:25:02 2015 +0100
23.3 @@ -341,7 +341,7 @@
23.4 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
23.5 Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
23.6 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
23.7 - ],scr = Prog ((term_of o the o (parse thy)) "empty_script")
23.8 + ],scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
23.9 }:rls);
23.10 *}
23.11 setup {* KEStore_Elems.add_rlss
23.12 @@ -389,7 +389,7 @@
23.13 Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6})
23.14 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
23.15 ],
23.16 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
23.17 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
23.18 }:rls);
23.19 *}
23.20 setup {* KEStore_Elems.add_rlss
23.21 @@ -438,7 +438,7 @@
23.22 Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
23.23 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
23.24 ],
23.25 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
23.26 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
23.27 }:rls);
23.28 *}
23.29 setup {* KEStore_Elems.add_rlss
23.30 @@ -473,7 +473,7 @@
23.31 Thm("sqrt_square_1",num_str @{thm sqrt_square_1})
23.32 (* sqrt a ^^^ 2 = a *)
23.33 ],
23.34 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
23.35 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
23.36 }:rls);
23.37 *}
23.38 setup {* KEStore_Elems.add_rlss
24.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Mon Dec 07 10:52:07 2015 +0100
24.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Dec 07 11:25:02 2015 +0100
24.3 @@ -128,7 +128,7 @@
24.4 ( (a = d + e/f) = ( (a - d) * f = e )) *)
24.5 Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
24.6 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
24.7 - ], scr = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);
24.8 + ], scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")}:rls);
24.9 *}
24.10 setup {* KEStore_Elems.add_rlss
24.11 [("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))] *}
25.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Mon Dec 07 10:52:07 2015 +0100
25.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Mon Dec 07 11:25:02 2015 +0100
25.3 @@ -58,20 +58,20 @@
25.4 (*.function for handling the cas-input "Simplify (2*a + 3*a)":
25.5 make a model which is already in ptree-internal format.*)
25.6 (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
25.7 - val (h,argl) = strip_comb ((term_of o the o (parse (Thy_Info.get_theory "Simplify")))
25.8 + val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info.get_theory "Simplify")))
25.9 "Simplify (2*a + 3*a)");
25.10 *)
25.11 fun argl2dtss t =
25.12 - [((term_of o the o (parse thy)) "Term", t),
25.13 - ((term_of o the o (parse thy)) "normalform",
25.14 - [(term_of o the o (parse thy)) "N"])
25.15 + [((Thm.term_of o the o (parse thy)) "Term", t),
25.16 + ((Thm.term_of o the o (parse thy)) "normalform",
25.17 + [(Thm.term_of o the o (parse thy)) "N"])
25.18 ]
25.19 (*| argl2dtss _ = error "Simplify.ML: wrong argument for argl2dtss"*);
25.20 *}
25.21 setup {* KEStore_Elems.add_cas
25.22 - [((term_of o the o (parse thy)) "Simplify",
25.23 + [((Thm.term_of o the o (parse thy)) "Simplify",
25.24 (("Isac", ["simplification"], ["no_met"]), argl2dtss)),
25.25 - ((term_of o the o (parse thy)) "Vereinfache",
25.26 + ((Thm.term_of o the o (parse thy)) "Vereinfache",
25.27 (("Isac", ["vereinfachen"], ["no_met"]), argl2dtss))]*}
25.28
25.29 end
25.30 \ No newline at end of file
26.1 --- a/src/Tools/isac/Knowledge/Test.sml Mon Dec 07 10:52:07 2015 +0100
26.2 +++ b/src/Tools/isac/Knowledge/Test.sml Mon Dec 07 11:25:02 2015 +0100
26.3 @@ -1,44 +1,44 @@
26.4 -val ttt = (term_of o the o (parse thy))
26.5 +val ttt = (Thm.term_of o the o (parse thy))
26.6 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e";
26.7 -val ttt = (term_of o the o (parse thy))
26.8 +val ttt = (Thm.term_of o the o (parse thy))
26.9 "(Try (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) e_e)";
26.10
26.11 -val ttt = (term_of o the o (parse thy))
26.12 +val ttt = (Thm.term_of o the o (parse thy))
26.13 "(Rewrite_Set SqRoot_simplify False) e_e ";
26.14 -val ttt = (term_of o the o (parseold thy))
26.15 +val ttt = (Thm.term_of o the o (parseold thy))
26.16 "%e_. (Rewrite_Set SqRoot_simplify False) e_e";
26.17 -val ttt = (term_of o the o (parseold thy))
26.18 +val ttt = (Thm.term_of o the o (parseold thy))
26.19 "Repeat (%e_. (Rewrite_Set SqRoot_simplify False)) e_e";
26.20
26.21 -val ttt = (term_of o the o (parse thy))
26.22 +val ttt = (Thm.term_of o the o (parse thy))
26.23 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.24 \[e_e]";
26.25 -val ttt = (term_of o the o (parse thy))
26.26 +val ttt = (Thm.term_of o the o (parse thy))
26.27 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.28 \((%e_. [e_e]) e_e)";
26.29 -val ttt = (term_of o the o (parse thy))
26.30 +val ttt = (Thm.term_of o the o (parse thy))
26.31 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.32 \((%e_. (let e_e = e_e in [e_e])) e_e)";
26.33 -val ttt = (term_of o the o (parse thy))
26.34 +val ttt = (Thm.term_of o the o (parse thy))
26.35 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.36 \((%e_. \
26.37 \ (let e_e = ((Rewrite_Set SqRoot_simplify False) e_e)\
26.38 \ in [e_e]))\
26.39 \ e_e)";
26.40 -val ttt = (term_of o the o (parse thy))
26.41 +val ttt = (Thm.term_of o the o (parse thy))
26.42 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.43 \((%ee_. (let e_e = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_e])) e_e)";
26.44
26.45 -val ttt = (term_of o the o (parse thy))
26.46 +val ttt = (Thm.term_of o the o (parse thy))
26.47 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.48 \(let e_e = \
26.49 \ (Repeat ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False)) e_e)\
26.50 \ in [e_e])";
26.51 (*----*)
26.52 -val ttt = (term_of o the o (parse thy))
26.53 +val ttt = (Thm.term_of o the o (parse thy))
26.54
26.55 (*----*)
26.56 -val ttt = (term_of o the o (parse thy))
26.57 +val ttt = (Thm.term_of o the o (parse thy))
26.58 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.59 \(let e_e = \
26.60 \ (Repeat\
26.61 @@ -46,7 +46,7 @@
26.62 \ e_e)\
26.63 \ e_e)\
26.64 \ in [e_e])";
26.65 -val ttt = (term_of o the o (parse thy))
26.66 +val ttt = (Thm.term_of o the o (parse thy))
26.67 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.68 \(let e_e = \
26.69 \ (Repeat\
26.70 @@ -55,7 +55,7 @@
26.71 \ e_e)\
26.72 \ e_e)\
26.73 \ in [e_e])";
26.74 -val ttt = (term_of o the o (parse thy))
26.75 +val ttt = (Thm.term_of o the o (parse thy))
26.76 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.77 \(let e_e = \
26.78 \ (Repeat\
26.79 @@ -68,30 +68,30 @@
26.80 atomty ttt;
26.81 atomt ttt;
26.82
26.83 -val ttt = (term_of o the o (parse thy))
26.84 +val ttt = (Thm.term_of o the o (parse thy))
26.85 "Script Testterm (g_::real) = \
26.86 \Repeat\
26.87 \ (Rewrite rmult_1 False) g_";
26.88 -val ttt = (term_of o the o (parse thy))
26.89 +val ttt = (Thm.term_of o the o (parse thy))
26.90 "Script Testterm (g_::real) = \
26.91 \Repeat\
26.92 \ (((Rewrite rmult_1 False)) Or ((Rewrite rmult_0 False))) g_";
26.93 -val ttt = (term_of o the o (parse thy))
26.94 +val ttt = (Thm.term_of o the o (parse thy))
26.95 "Script Testterm (g_::real) = \
26.96 \Repeat\
26.97 \ ((Repeat (Rewrite rmult_1 False)) Or (Repeat (Rewrite rmult_0 False))) g_";
26.98 -val ttt = (term_of o the o (parse thy))
26.99 +val ttt = (Thm.term_of o the o (parse thy))
26.100 "Script Testterm (g_::real) = \
26.101 \Repeat\
26.102 \ ((Repeat (Rewrite rmult_1 False)) Or\
26.103 \ (Repeat (Rewrite rmult_0 False))) g_";
26.104 -val ttt = (term_of o the o (parse thy))
26.105 +val ttt = (Thm.term_of o the o (parse thy))
26.106 "Script Testterm (g_::real) = \
26.107 \Repeat\
26.108 \ ((Repeat (Rewrite rmult_1 False)) Or\
26.109 \ (Repeat (Rewrite rmult_0 False)) Or\
26.110 \ (Repeat (Rewrite rmult_0 False))) g_";
26.111 -val ttt = (term_of o the o (parse thy))
26.112 +val ttt = (Thm.term_of o the o (parse thy))
26.113 "Script Testterm (g_::real) = \
26.114 \Repeat\
26.115 \ ((Try Repeat (Rewrite rmult_1 False)) Or\
26.116 @@ -117,7 +117,7 @@
26.117
26.118
26.119 atomt ttt;
26.120 -val ttt = (term_of o the o (parse thy))
26.121 +val ttt = (Thm.term_of o the o (parse thy))
26.122 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.123 \(let e_e = \
26.124 \ ((Repeat\
26.125 @@ -127,26 +127,26 @@
26.126 atomty ttt;
26.127
26.128
26.129 -val ttt = (term_of o the o (parse thy))
26.130 +val ttt = (Thm.term_of o the o (parse thy))
26.131 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ yyy";
26.132 atomty ttt;
26.133 -val ttt = (term_of o the o (parse thy))
26.134 +val ttt = (Thm.term_of o the o (parse thy))
26.135 "(Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
26.136 \ (Rewrite_Set SqRoot_simplify False)";
26.137 atomty ttt;
26.138 -val ttt = (term_of o the o (parse thy))
26.139 +val ttt = (Thm.term_of o the o (parse thy))
26.140 "(Repeat\
26.141 \ ((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@\
26.142 \ (Rewrite_Set SqRoot_simplify False))) e_e";
26.143 atomty ttt;
26.144 -val ttt = (term_of o the o (parseold thy))
26.145 +val ttt = (Thm.term_of o the o (parseold thy))
26.146 "(let e_e = Repeat xxx e_e in [e_::bool])";
26.147 atomty ttt;
26.148 -val ttt = (term_of o the o (parseold thy))
26.149 +val ttt = (Thm.term_of o the o (parseold thy))
26.150 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.151 \(let e_e = Repeat (xxx) e_e in [e_::bool])";
26.152 atomty ttt;
26.153 -val ttt = (term_of o the o (parseold thy))
26.154 +val ttt = (Thm.term_of o the o (parseold thy))
26.155 "Script Solve_linear (e_e::bool) (v_v::real)= \
26.156 \(let e_e =\
26.157 \ Repeat\
27.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Dec 07 10:52:07 2015 +0100
27.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Dec 07 11:25:02 2015 +0100
27.3 @@ -247,7 +247,7 @@
27.4 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
27.5
27.6 Calc ("Atools.ident",eval_ident "#ident_")],
27.7 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
27.8 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
27.9 }:rls;
27.10 *}
27.11 ML {*
27.12 @@ -292,7 +292,7 @@
27.13 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
27.14
27.15 Calc ("Atools.ident",eval_ident "#ident_")],
27.16 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
27.17 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
27.18 }:rls;
27.19 *}
27.20 setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))] *}
27.21 @@ -306,7 +306,7 @@
27.22 rules =
27.23 [Thm ("sym_add_assoc",num_str (@{thm add.assoc} RS @{thm sym})),
27.24 Thm ("sym_rmult_assoc",num_str (@{thm rmult_assoc} RS @{thm sym}))],
27.25 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
27.26 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
27.27 }:rls;
27.28
27.29 val ac_plus_times =
27.30 @@ -319,7 +319,7 @@
27.31 Thm ("rmult_commute",num_str @{thm rmult_commute}),
27.32 Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
27.33 Thm ("rmult_assoc",num_str @{thm rmult_assoc})],
27.34 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
27.35 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
27.36 }:rls;
27.37
27.38 (*todo: replace by Rewrite("rnorm_equation_add",num_str @{thm rnorm_equation_add)*)
27.39 @@ -328,7 +328,7 @@
27.40 erls = tval_rls, srls = e_rls, calc = [], errpatts = [],
27.41 rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add})
27.42 ],
27.43 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
27.44 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
27.45 }:rls;
27.46 *}
27.47 ML {*
27.48 @@ -435,7 +435,7 @@
27.49 Thm ("radd_0",num_str @{thm radd_0}),
27.50 Thm ("radd_0_right",num_str @{thm radd_0_right})
27.51 ],
27.52 - scr = Prog ((term_of o the o (parse thy)) "empty_script")
27.53 + scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
27.54 (*since 040209 filled by prep_rls': STest_simplify*)
27.55 }:rls;
27.56 *}
27.57 @@ -455,7 +455,7 @@
27.58 Thm ("risolate_root_add",num_str @{thm risolate_root_add}),
27.59 Thm ("risolate_root_mult",num_str @{thm risolate_root_mult}),
27.60 Thm ("risolate_root_div",num_str @{thm risolate_root_div}) ],
27.61 - scr = Prog ((term_of o the o (parse thy))
27.62 + scr = Prog ((Thm.term_of o the o (parse thy))
27.63 "empty_script")
27.64 }:rls;
27.65
27.66 @@ -471,7 +471,7 @@
27.67 Thm ("constant_square",num_str @{thm constant_square}),
27.68 Thm ("constant_mult_square",num_str @{thm constant_mult_square})
27.69 ],
27.70 - scr = Prog ((term_of o the o (parse thy))
27.71 + scr = Prog ((Thm.term_of o the o (parse thy))
27.72 "empty_script")
27.73 }:rls;
27.74 *}
27.75 @@ -543,7 +543,7 @@
27.76 [("#Given" ,"boolTestGiven g_g"),
27.77 ("#Find" ,"boolTestFind f_f")],
27.78 []))*)] *}
27.79 -(*val ttt = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)";
27.80 +(*val ttt = (Thm.term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)";
27.81
27.82 ------ 25.8.01*)
27.83
27.84 @@ -641,7 +641,7 @@
27.85 | varids (Abs(a,T,t)) = union op = [a] (varids t)
27.86 | varids (t1 $ t2) = union op = (varids t1) (varids t2)
27.87 | varids _ = [];
27.88 -(*> val t = term_of (hd (parse Diophant.thy "x"));
27.89 +(*> val t = Thm.term_of (hd (parse Diophant.thy "x"));
27.90 val t = Free ("x","?DUMMY") : term
27.91 > varids t;
27.92 val it = [] : string list [] !!! *)
27.93 @@ -737,11 +737,11 @@
27.94 assoc_rls' @{theory} "matches",
27.95 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]))] *}
27.96 (*
27.97 - val e_e = (term_of o the o (parse thy)) "e_e::bool";
27.98 - val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
27.99 + val e_e = (Thm.term_of o the o (parse thy)) "e_e::bool";
27.100 + val ve = (Thm.term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
27.101 val env = [(e_,ve)];
27.102
27.103 - val pre = (term_of o the o (parse thy))
27.104 + val pre = (Thm.term_of o the o (parse thy))
27.105 "(matches (a + b*v_v ^^^2 = 0, e_e::bool)) |" ^
27.106 "(matches ( b*v_v ^^^2 = 0, e_e::bool)) |" ^
27.107 "(matches (a + v_v ^^^2 = 0, e_e::bool)) |" ^
27.108 @@ -1221,7 +1221,7 @@
27.109 Calc ("Groups.times_class.times", eval_binop "#mult_"),
27.110 Calc ("Atools.pow", eval_binop "#power_")
27.111 ],
27.112 - scr = EmptyScr(*Prog ((term_of o the o (parse thy))
27.113 + scr = EmptyScr(*Prog ((Thm.term_of o the o (parse thy))
27.114 scr_make_polytest)*)
27.115 }:rls;
27.116 *}
27.117 @@ -1355,7 +1355,7 @@
27.118 Calc ("Atools.pow", eval_binop "#power_")
27.119 ],
27.120 scr = EmptyScr
27.121 -(*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
27.122 +(*Script ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
27.123 }:rls;
27.124 *}
27.125 setup {* KEStore_Elems.add_rlss
28.1 --- a/src/Tools/isac/ProgLang/Tools.sml Mon Dec 07 10:52:07 2015 +0100
28.2 +++ b/src/Tools/isac/ProgLang/Tools.sml Mon Dec 07 11:25:02 2015 +0100
28.3 @@ -10,7 +10,7 @@
28.4 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
28.5 | eval_var _ _ _ _ = raise GO_ON;
28.6 (*
28.7 -> val t = (term_of o the o (parse thy)) "Var (A=a*(b::real))";
28.8 +> val t = (Thm.term_of o the o (parse thy)) "Var (A=a*(b::real))";
28.9 > val op_ = "Var";
28.10 > val eval_fn = the (assoc (!eval_list, op_));
28.11 > get_pair op_ eval_fn t;
28.12 @@ -27,14 +27,14 @@
28.13 fun eval_Length (thmid:string) (op_:string)
28.14 (t as (Const(op0,t0) $ arg)) thy =
28.15 let
28.16 - val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg;
28.17 + val t' = ((Thm.term_of_num HOLogic.realT) o length o isalist2list) arg;
28.18 val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
28.19 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
28.20 | eval_Length _ _ _ _ = raise GO_ON;
28.21 (*
28.22 > val thmid = "#Length_"; val op_ = "Length";
28.23 > val s = "Length [A = a * b, a // #2 = #2]";
28.24 -> val (t as (Const(op0,t0) $ arg)) = (term_of o the o (parse thy)) s;
28.25 +> val (t as (Const(op0,t0) $ arg)) = (Thm.term_of o the o (parse thy)) s;
28.26 > val (SOME (id,t')) = eval_Length thmid op_ t;
28.27 val id = "#Length_[A = a * b, a // #2 = #2]" : string
28.28 val t' = Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
28.29 @@ -47,7 +47,7 @@
28.30 \else hd [A = a * b, a // #2 = #2]";
28.31
28.32 > (Thm.global_cterm_of thy) t';
28.33 -> val t = (term_of o the o (parse thy)) s;
28.34 +> val t = (Thm.term_of o the o (parse thy)) s;
28.35 > val eval_fn = the (assoc (!eval_list, op_));
28.36 > val (SOME(_,t')) = get_pair op_ eval_fn t;
28.37 val t' = Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
28.38 @@ -87,7 +87,7 @@
28.39 (*
28.40 > val thmid = "#Nth_"; val op_ = "Nth";
28.41 > val s = "Nth #2 [A = a * b, a // #2 = #2]";
28.42 -> val t = (term_of o the o (parse thy)) s;
28.43 +> val t = (Thm.term_of o the o (parse thy)) s;
28.44 > eval_Nth thmid op_ t;
28.45
28.46 > val eval_fn = the (assoc (!eval_list, op_));
29.1 --- a/src/Tools/isac/ProgLang/Tools.thy Mon Dec 07 10:52:07 2015 +0100
29.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Mon Dec 07 11:25:02 2015 +0100
29.3 @@ -51,8 +51,8 @@
29.4 ML {* (*the former Tools.ML*)
29.5 (* auxiliary functions for scripts WN.9.00*)
29.6 (*11.02: for equation solving only*)
29.7 -val UniversalList = (term_of o the o (parse @{theory})) "UniversalList";
29.8 -val EmptyList = (term_of o the o (parse @{theory})) "[]::bool list";
29.9 +val UniversalList = (Thm.term_of o the o (parse @{theory})) "UniversalList";
29.10 +val EmptyList = (Thm.term_of o the o (parse @{theory})) "[]::bool list";
29.11
29.12 (*+ for Or_to_List +*)
29.13 fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)
29.14 @@ -76,11 +76,11 @@
29.15 > val t' = or2list t;
29.16 > term2str t';
29.17 "[]"
29.18 -> val t=(term_of o the o (parse thy)) "x=3";
29.19 +> val t=(Thm.term_of o the o (parse thy)) "x=3";
29.20 > val t' = or2list t;
29.21 > term2str t';
29.22 "[x = 3]"
29.23 -> val t=(term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
29.24 +> val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
29.25 > val t' = or2list t;
29.26 > term2str t';
29.27 "[x = #3, x = #-3, x = #0]" : string *)
29.28 @@ -103,7 +103,7 @@
29.29 in SOME (term_to_string''' thy prop, prop) end
29.30 | eval_matches _ _ _ _ = NONE;
29.31 (*
29.32 -> val t = (term_of o the o (parse thy))
29.33 +> val t = (Thm.term_of o the o (parse thy))
29.34 "matches (?x = 0) (1 * x ^^^ 2 = 0)";
29.35 > eval_matches "/thmid/" "/op_/" t thy;
29.36 val it =
29.37 @@ -111,7 +111,7 @@
29.38 ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
29.39 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
29.40
29.41 -> val t = (term_of o the o (parse thy))
29.42 +> val t = (Thm.term_of o the o (parse thy))
29.43 "matches (?a = #0) (#1 * x ^^^ #2 = #0)";
29.44 > eval_matches "/thmid/" "/op_/" t thy;
29.45 val it =
29.46 @@ -119,7 +119,7 @@
29.47 ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
29.48 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
29.49
29.50 -> val t = (term_of o the o (parse thy))
29.51 +> val t = (Thm.term_of o the o (parse thy))
29.52 "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
29.53 > eval_matches "/thmid/" "/op_/" t thy;
29.54 val it =
29.55 @@ -127,7 +127,7 @@
29.56 ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
29.57 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
29.58
29.59 -> val t = (term_of o the o (parse thy))
29.60 +> val t = (Thm.term_of o the o (parse thy))
29.61 "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
29.62 > eval_matches "/thmid/" "/op_/" t thy;
29.63 val it =
29.64 @@ -135,7 +135,7 @@
29.65 ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
29.66 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
29.67 ----- before ?patterns ---:
29.68 -> val t = (term_of o the o (parse thy))
29.69 +> val t = (Thm.term_of o the o (parse thy))
29.70 "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
29.71 > eval_matches "/thmid/" "/op_/" t thy;
29.72 SOME
29.73 @@ -143,13 +143,13 @@
29.74 Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
29.75 : (string * term) option
29.76
29.77 -> val t = (term_of o the o (parse thy))
29.78 +> val t = (Thm.term_of o the o (parse thy))
29.79 "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
29.80 > eval_matches "/thmid/" "/op_/" t thy;
29.81 SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
29.82 Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
29.83
29.84 -> val t = (term_of o the o (parse thy))
29.85 +> val t = (Thm.term_of o the o (parse thy))
29.86 "matches (a = b) (x + #1 + #-1 * #2 = #0)";
29.87 > eval_matches "/thmid/" "/op_/" t thy;
29.88 SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
29.89 @@ -199,7 +199,7 @@
29.90 Trueprop $ (mk_equality (t, l)))
29.91 | eval_lhs _ _ _ _ = NONE;
29.92 (*
29.93 -> val t = (term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
29.94 +> val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
29.95 > val SOME (id,t') = eval_lhs 0 0 t 0;
29.96 val id = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
29.97 > term2str t';
30.1 --- a/src/Tools/isac/ProgLang/calculate.sml Mon Dec 07 10:52:07 2015 +0100
30.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Mon Dec 07 11:25:02 2015 +0100
30.3 @@ -103,33 +103,33 @@
30.4 | get_pair _ _ _ _ = NONE
30.5
30.6 (*
30.7 -> val t = (term_of o the o (parse thy)) "#3 + #4";
30.8 +> val t = (Thm.term_of o the o (parse thy)) "#3 + #4";
30.9 > val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
30.10 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
30.11 > term2str t';
30.12 > atomty t';
30.13 >
30.14 -> val t = (term_of o the o (parse thy)) "(a + #3) + #4";
30.15 +> val t = (Thm.term_of o the o (parse thy)) "(a + #3) + #4";
30.16 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
30.17 > term2str t';
30.18 >
30.19 -> val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
30.20 +> val t = (Thm.term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
30.21 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
30.22 > term2str t';
30.23 >
30.24 -> val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
30.25 +> val t = (Thm.term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
30.26 > atomty t;
30.27 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
30.28 > term2str t';
30.29 > val it = "#3 + (#4 + a) = #7 + a" : string
30.30 >
30.31 >
30.32 -> val t = (term_of o the o (parse thy)) "#-4//#-2";
30.33 +> val t = (Thm.term_of o the o (parse thy)) "#-4//#-2";
30.34 > val eval_fn = the (assoc (!eval_list, "cancel"));
30.35 > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
30.36 > term2str t';
30.37 >
30.38 -> val t = (term_of o the o (parse thy)) "#2^^^#3";
30.39 +> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
30.40 > eval_binop "xxx" "pow" t thy;
30.41 > val eval_fn = (eval_binop "xxx")
30.42 > : string -> term -> theory -> (string * term) option;
30.43 @@ -139,43 +139,43 @@
30.44 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
30.45 > term2str t';
30.46 >
30.47 -> val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
30.48 +> val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
30.49 > val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));
30.50 > val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;
30.51 > term2str t';
30.52 >
30.53 -> val t = (term_of o the o (parse thy)) "#0 < #4";
30.54 +> val t = (Thm.term_of o the o (parse thy)) "#0 < #4";
30.55 > val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less"));
30.56 > val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
30.57 > term2str t';
30.58 -> val t = (term_of o the o (parse thy)) "#0 < #-4";
30.59 +> val t = (Thm.term_of o the o (parse thy)) "#0 < #-4";
30.60 > val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
30.61 > term2str t';
30.62 >
30.63 -> val t = (term_of o the o (parse thy)) "#3 is_const";
30.64 +> val t = (Thm.term_of o the o (parse thy)) "#3 is_const";
30.65 > val eval_fn = the (assoc (!eval_list, "is'_const"));
30.66 > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
30.67 > term2str t';
30.68 -> val t = (term_of o the o (parse thy)) "a is_const";
30.69 +> val t = (Thm.term_of o the o (parse thy)) "a is_const";
30.70 > val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
30.71 > term2str t';
30.72 >
30.73 -> val t = (term_of o the o (parse thy)) "#6//(#8::real)";
30.74 +> val t = (Thm.term_of o the o (parse thy)) "#6//(#8::real)";
30.75 > val eval_fn = the (assoc (!eval_list, "cancel"));
30.76 > val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
30.77 > term2str t';
30.78 >
30.79 -> val t = (term_of o the o (parse thy)) "sqrt #12";
30.80 +> val t = (Thm.term_of o the o (parse thy)) "sqrt #12";
30.81 > val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
30.82 > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
30.83 > term2str t';
30.84 > val it = "sqrt #12 = #2 * sqrt #3 " : string
30.85 >
30.86 -> val t = (term_of o the o (parse thy)) "sqrt #9";
30.87 +> val t = (Thm.term_of o the o (parse thy)) "sqrt #9";
30.88 > val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
30.89 > term2str t';
30.90 >
30.91 -> val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
30.92 +> val t = (Thm.term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
30.93 > val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
30.94 > val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
30.95 > term2str t';
30.96 @@ -217,19 +217,19 @@
30.97
30.98 -------------------------------------------------------------------6.8.02:
30.99 val thy = SqRoot.thy;
30.100 - val t = (term_of o the o (parse thy)) "1+2";
30.101 + val t = (Thm.term_of o the o (parse thy)) "1+2";
30.102 get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t;
30.103 val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option
30.104 -------------------------------------------------------------------6.8.02:
30.105 - val t = (term_of o the o (parse thy)) "-1";
30.106 + val t = (Thm.term_of o the o (parse thy)) "-1";
30.107 atomty t;
30.108 - val t = (term_of o the o (parse thy)) "0";
30.109 + val t = (Thm.term_of o the o (parse thy)) "0";
30.110 atomty t;
30.111 - val t = (term_of o the o (parse thy)) "1";
30.112 + val t = (Thm.term_of o the o (parse thy)) "1";
30.113 atomty t;
30.114 - val t = (term_of o the o (parse thy)) "2";
30.115 + val t = (Thm.term_of o the o (parse thy)) "2";
30.116 atomty t;
30.117 - val t = (term_of o the o (parse thy)) "999999999";
30.118 + val t = (Thm.term_of o the o (parse thy)) "999999999";
30.119 atomty t;
30.120 -------------------------------------------------------------------6.8.02:
30.121
31.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Dec 07 10:52:07 2015 +0100
31.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Dec 07 11:25:02 2015 +0100
31.3 @@ -255,8 +255,8 @@
31.4 fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
31.5
31.6 fun subs'2subst thy (s:subs') =
31.7 - (((map (apfst (term_of o the o (parse thy))))
31.8 - o (map (apsnd (term_of o the o (parse thy))))) s):subst;
31.9 + (((map (apfst (Thm.term_of o the o (parse thy))))
31.10 + o (map (apsnd (Thm.term_of o the o (parse thy))))) s):subst;
31.11
31.12 (*.variants of rewrite.*)
31.13 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
31.14 @@ -319,7 +319,7 @@
31.15
31.16 (*Thm.make_thm added to Pure/thm.ML*)
31.17 fun mk_thm thy str =
31.18 - let val t = (term_of o the o (parse thy)) str
31.19 + let val t = (Thm.term_of o the o (parse thy)) str
31.20 val t' = case t of
31.21 Const ("==>",_) $ _ $ _ => t
31.22 | _ => Trueprop $ t
31.23 @@ -329,7 +329,7 @@
31.24 val thm = realpow_twoI;
31.25
31.26 val t1 = (#prop o rep_thm) (num_str thm);
31.27 - val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
31.28 + val t2 = Trueprop $ ((Thm.term_of o the o (parse thy)) str);
31.29 t1 = t2;
31.30 val it = true : bool ... !!!
31.31 val th1 = (num_str thm);
31.32 @@ -342,7 +342,7 @@
31.33 val thm = real_mult_div_cancel2;
31.34
31.35 val t1 = (#prop o rep_thm) (num_str thm);
31.36 - val t2 = ((term_of o the o (parse thy)) str);
31.37 + val t2 = ((Thm.term_of o the o (parse thy)) str);
31.38 t1 = t2;
31.39 val it = false : bool ... Var .. Free
31.40 val th1 = (num_str thm);
31.41 @@ -356,7 +356,7 @@
31.42 ((goal thy);(topthm()) o ) str; *)
31.43 (*assume rejects scheme variables
31.44 assume ((Thm.global_cterm_of thy) (Trueprop $
31.45 - (term_of o the o (parse thy)) str)); *)
31.46 + (Thm.term_of o the o (parse thy)) str)); *)
31.47
31.48
31.49 (* outcommented 18.11.xx, xx < 02 -------
31.50 @@ -426,7 +426,7 @@
31.51 fun parse' (thy:theory') (ct:cterm') =
31.52 case parse (assoc_thy thy) ct of
31.53 NONE => NONE
31.54 - | SOME ct => SOME ((term2str (term_of ct)):cterm');
31.55 + | SOME ct => SOME ((term2str (Thm.term_of ct)):cterm');
31.56
31.57
31.58 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
31.59 @@ -435,7 +435,7 @@
31.60 let val thy = assoc_thy thy';
31.61 in
31.62 case rewrite_ thy ((the o assoc')(!rew_ord',rew_ord))(assoc_rls rls)
31.63 - put_asm ((assoc_thm' thy) thm) ((term_of o the o (parse thy)) ct) of
31.64 + put_asm ((assoc_thm' thy) thm) ((Thm.term_of o the o (parse thy)) ct) of
31.65 NONE => NONE
31.66 | SOME (t, ts) => SOME (term2str t, terms2str ts)
31.67 end;
31.68 @@ -445,7 +445,7 @@
31.69 fun rewrite_set (thy':theory') (put_asm:bool) (rls:rls') (ct:cterm') =
31.70 let val thy = (assoc_thy thy');
31.71 in
31.72 - case rewrite_set_ thy put_asm (assoc_rls rls) ((term_of o the o (parse thy)) ct) of
31.73 + case rewrite_set_ thy put_asm (assoc_rls rls) ((Thm.term_of o the o (parse thy)) ct) of
31.74 NONE => NONE
31.75 | SOME (t, ts) => SOME (term2str t, terms2str ts)
31.76 end;
31.77 @@ -456,7 +456,7 @@
31.78
31.79 fun get_calculation' (thy:theory') op_ (ct:cterm') =
31.80 case get_calculation_ (assoc_thy thy) op_
31.81 - ((uminus_to_string o term_of o the o
31.82 + ((uminus_to_string o Thm.term_of o the o
31.83 (parse (assoc_thy thy))) ct) of
31.84 NONE => NONE
31.85 | SOME (thmid, thm) =>
31.86 @@ -466,7 +466,7 @@
31.87 let val thy = (assoc_thy thy');
31.88 in
31.89 case calculate_ thy op_
31.90 - ((term_of o the o (parse thy)) ct) of
31.91 + ((Thm.term_of o the o (parse thy)) ct) of
31.92 NONE => NONE
31.93 | SOME (ct,(thmID,thm)) =>
31.94 SOME (term2str ct,
31.95 @@ -484,7 +484,7 @@
31.96 in
31.97 case rewrite_ thy
31.98 ((the o assoc')(!rew_ord',rew_ord)) (assoc_rls rls)
31.99 - put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
31.100 + put_asm (*sub*)thm ((Thm.term_of o the o (parse thy)) ct) of
31.101 NONE => NONE
31.102 | SOME (ctm, ctms) =>
31.103 SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)
31.104 @@ -499,7 +499,7 @@
31.105 val rls = assoc_rls rls
31.106 val subst = subs'2subst thy subs'
31.107 in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
31.108 - ((term_of o the o (parse thy)) ct) of
31.109 + ((Thm.term_of o the o (parse thy)) ct) of
31.110 NONE => NONE
31.111 | SOME (t, ts) => SOME (term2str t, terms2str ts)
31.112 end;
31.113 @@ -527,7 +527,7 @@
31.114 Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
31.115 rules = [Calc ("matches",eval_matches "")
31.116 ],
31.117 - scr = Prog ((term_of o the o (parse thy))
31.118 + scr = Prog ((Thm.term_of o the o (parse thy))
31.119 "empty_script")
31.120 }:rls;
31.121
31.122 @@ -535,7 +535,7 @@
31.123
31.124 rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false test_rls
31.125 ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
31.126 - val xxx = (term_of o the o (parse thy))
31.127 + val xxx = (Thm.term_of o the o (parse thy))
31.128 "matches (?a = ?b) (x = #0)";
31.129 eval_matches """" xxx thy;
31.130 SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
32.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Mon Dec 07 10:52:07 2015 +0100
32.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Mon Dec 07 11:25:02 2015 +0100
32.3 @@ -18,7 +18,7 @@
32.4 [Type ("bool",[])]),_])) $ t) = true
32.5 | is_booll_dsc _ = false;
32.6 (*
32.7 -> val t = (term_of o the o (parse thy)) "relations";
32.8 +> val t = (Thm.term_of o the o (parse thy)) "relations";
32.9 > atomtyp (type_of t);
32.10 *** Type (fun,[
32.11 *** Type (List.list,[
32.12 @@ -41,19 +41,19 @@
32.13 > is_list_dsc t;
32.14 val it = true : bool
32.15
32.16 -> val t = (term_of o the o (parse thy))
32.17 +> val t = (Thm.term_of o the o (parse thy))
32.18 "additional_relations [a=b,c=(d::real)]";
32.19 > is_list_dsc t;
32.20 val it = true : bool
32.21 > is_list_dsc (head_of t);
32.22 val it = true : bool
32.23
32.24 -> val t = (term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)";
32.25 +> val t = (Thm.term_of o the o (parse thy))"max_relation (A=#2*a*b-a^^^#2)";
32.26 > is_list_dsc t;
32.27 val it = false : bool
32.28 > is_list_dsc (head_of t);
32.29 val it = false : bool
32.30 -> val t = (term_of o the o (parse thy)) "testdscforlist";
32.31 +> val t = (Thm.term_of o the o (parse thy)) "testdscforlist";
32.32 > is_list_dsc (head_of t);
32.33 val it = true : bool
32.34 *)
32.35 @@ -64,7 +64,7 @@
32.36 (*
32.37 > val t = str2term "someList"; is_unl t;
32.38 val it = true : bool
32.39 -> val t = (term_of o the o (parse thy)) "maximum";
32.40 +> val t = (Thm.term_of o the o (parse thy)) "maximum";
32.41 > is_unl t;
32.42 val it = false : bool
32.43 *)
32.44 @@ -101,17 +101,17 @@
32.45 val Const (_, Type ("fun", [Type ("fun", _), Type ("Tools.una",[])])) $ _ = t;
32.46 is_dsc t1;
32.47
32.48 -> val t = (term_of o the o (parse thy)) "maximum";
32.49 +> val t = (Thm.term_of o the o (parse thy)) "maximum";
32.50 > is_dsc t;
32.51 val it = true : bool
32.52 -> val t = (term_of o the o (parse thy)) "testdscforlist";
32.53 +> val t = (Thm.term_of o the o (parse thy)) "testdscforlist";
32.54 > is_dsc t;
32.55 val it = true : bool
32.56
32.57 -> val t = (head_of o term_of o the o (parse thy)) "maximum A";
32.58 +> val t = (head_of o Thm.term_of o the o (parse thy)) "maximum A";
32.59 > is_dsc t;
32.60 val it = true : bool
32.61 -> val t = (head_of o term_of o the o (parse thy))
32.62 +> val t = (head_of o Thm.term_of o the o (parse thy))
32.63 "fixedValues [R=(R::real)]";
32.64 > is_dsc t;
32.65 val it = true : bool
32.66 @@ -121,12 +121,12 @@
32.67 (*make the term 'Subproblem (domID, pblID)' to a formula for frontend;
32.68 needs to be here after def. Subproblem in Script.thy*)
32.69 val t as (subpbl_t $ (pair_t $ Free (domID,_) $ pblID)) =
32.70 - (term_of o the o (parse @{theory Script}))
32.71 + (Thm.term_of o the o (parse @{theory Script}))
32.72 "Subproblem (Isac,[equation,univar])";
32.73 val t as (pbl_t $ _) =
32.74 - (term_of o the o (parse @{theory Script}))
32.75 + (Thm.term_of o the o (parse @{theory Script}))
32.76 "Problem (Isac,[equation,univar])";
32.77 -val Free (_, ID_type) = (term_of o the o (parse @{theory Script})) "x::ID";
32.78 +val Free (_, ID_type) = (Thm.term_of o the o (parse @{theory Script})) "x::ID";
32.79
32.80
32.81 fun subpbl domID pblID =
32.82 @@ -318,16 +318,16 @@
32.83 (** for automatic creation of scripts from rls **)
32.84 (* naming of identifiers in scripts ???...
32.85 not accepted !!!...
32.86 -((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_::'z) = t_";
32.87 -((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o
32.88 +((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory})) "(t_::'z) = t_";
32.89 +((inst_abs @{theory}) o Thm.term_of o (the:cterm option -> cterm) o
32.90 (parse @{theory})) "(_t::'z) = _t";
32.91 *)
32.92 -((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t::'z) = t";
32.93 -((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o
32.94 +((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory})) "(t::'z) = t";
32.95 +((inst_abs @{theory}) o Thm.term_of o (the:cterm option -> cterm) o
32.96 (parse @{theory})) "(t't::'z) = t't";
32.97 -((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_t::'z) = t_t";
32.98 +((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory})) "(t_t::'z) = t_t";
32.99
32.100 -((inst_abs @{theory}) o term_of o the o (parse @{theory}))
32.101 +((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory}))
32.102 "Script Stepwise (t_t::'z) =\
32.103 \(Repeat\
32.104 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
32.105 @@ -335,7 +335,7 @@
32.106 \ (Try (Repeat (Rewrite mult_commute False)))) \
32.107 \ t_t)";
32.108 val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*)
32.109 - ((inst_abs @{theory}) o term_of o the o (parse @{theory}))
32.110 + ((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory}))
32.111 "Script Stepwise (t_t::'z) =\
32.112 \(Repeat\
32.113 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
32.114 @@ -345,7 +345,7 @@
32.115 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body
32.116 are inconsistent !!!*)
32.117 val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)
32.118 - ((inst_abs @{theory}) o term_of o the o (parse @{theory}))
32.119 + ((inst_abs @{theory}) o Thm.term_of o the o (parse @{theory}))
32.120 "Script Stepwise_inst (t_t::'z) (v::real) =\
32.121 \(Repeat\
32.122 \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \
32.123 @@ -353,31 +353,31 @@
32.124 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] mult_commute False)))) \
32.125 \ t_t)";
32.126 val Repeat $ _ =
32.127 - ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
32.128 + ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory}))
32.129 "Repeat (Rewrite real_diff_minus False t)";
32.130 val Try $ _ =
32.131 - ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
32.132 + ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory}))
32.133 "Try (Rewrite real_diff_minus False t)";
32.134 val Cal $ _ =
32.135 - ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
32.136 + ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory}))
32.137 "Calculate PLUS";
32.138 val Ca1 $ _ =
32.139 - ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
32.140 + ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory}))
32.141 "Calculate1 PLUS";
32.142 val Rew $ (Free (_,IDtype)) $ _ $ t =
32.143 - ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
32.144 + ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory}))
32.145 "Rewrite real_diff_minus False t";
32.146 val Rew_Inst $ Subs $ _ $ _ =
32.147 - ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
32.148 + ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory}))
32.149 "Rewrite_Inst [(bdv,v)] real_diff_minus False";
32.150 val Rew_Set $ _ $ _ =
32.151 - ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
32.152 + ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory}))
32.153 "Rewrite_Set real_diff_minus False";
32.154 val Rew_Set_Inst $ _ $ _ $ _ =
32.155 - ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
32.156 + ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory}))
32.157 "Rewrite_Set_Inst [(bdv,v)] real_diff_minus False";
32.158 val SEq $ _ $ _ $ _ =
32.159 - ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
32.160 + ((inst_abs @{theory}) o Thm.term_of o the o (parseN @{theory}))
32.161 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
32.162 \ (Try (Repeat (Rewrite add_commute False))) @@ \
32.163 \ (Try (Repeat (Rewrite mult_commute False)))) t";
33.1 --- a/src/Tools/isac/ProgLang/termC.sml Mon Dec 07 10:52:07 2015 +0100
33.2 +++ b/src/Tools/isac/ProgLang/termC.sml Mon Dec 07 11:25:02 2015 +0100
33.3 @@ -38,7 +38,7 @@
33.4 | atol n (T::Ts) = (ato n T ^ atol n Ts)
33.5 in tracing (ato 0 t ^ "\n") end;
33.6 (*
33.7 -> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
33.8 +> val T = (type_of o Thm.term_of o the o (parse thy)) "a::[real,int] => nat";
33.9 > atomtyp T;
33.10 *** Type (fun,[
33.11 *** Type (RealDef.real,[])
33.12 @@ -191,11 +191,11 @@
33.13 fun is_num (Free (s,_)) = if is_numeral s then true else false
33.14 | is_num _ = false;
33.15 (*>
33.16 -> is_num ((term_of o the o (parse thy)) "#1");
33.17 +> is_num ((Thm.term_of o the o (parse thy)) "#1");
33.18 val it = true : bool
33.19 -> is_num ((term_of o the o (parse thy)) "#-1");
33.20 +> is_num ((Thm.term_of o the o (parse thy)) "#-1");
33.21 val it = true : bool
33.22 -> is_num ((term_of o the o (parse thy)) "a123");
33.23 +> is_num ((Thm.term_of o the o (parse thy)) "a123");
33.24 val it = false : bool
33.25 *)
33.26
33.27 @@ -292,7 +292,7 @@
33.28 fun list2isalist T [] = Const("List.list.Nil",mk_listT T)
33.29 | list2isalist T (t::ts) = (list_const T) $ t $ (list2isalist T ts);
33.30 (*
33.31 -> val tt = (term_of o the o (parse thy)) "R=(R::real)";
33.32 +> val tt = (Thm.term_of o the o (parse thy)) "R=(R::real)";
33.33 > val TT = type_of tt;
33.34 > val ss = list2isalist TT [tt,tt,tt];
33.35 > (Thm.global_cterm_of thy) ss;
33.36 @@ -602,7 +602,7 @@
33.37 Const ("Groups.times_class.times", [T, T] ---> T) $ (term_of_num T fact) $
33.38 (Const (op_, T --> T) $ term_of_num T root);
33.39 (*
33.40 -val T = (type_of o term_of o the) (parse thy "#12::real");
33.41 +val T = (type_of o Thm.term_of o the) (parse thy "#12::real");
33.42 val t = mk_factroot "SqRoot.sqrt" T 2 3;
33.43 (Thm.global_cterm_of thy) t;
33.44 val it = "#2 * sqrt #3 " : cterm
33.45 @@ -633,10 +633,10 @@
33.46 | const_in str (Abs (_,_,body)) = const_in str body
33.47 | const_in str (f$u) = const_in str f orelse const_in str u;
33.48 (*
33.49 -> val t = (term_of o the o (parse thy)) "6 + 5 * sqrt 4 + 3";
33.50 +> val t = (Thm.term_of o the o (parse thy)) "6 + 5 * sqrt 4 + 3";
33.51 > const_in "sqrt" t;
33.52 val it = true : bool
33.53 -> val t = (term_of o the o (parse thy)) "6 + 5 * 4 + 3";
33.54 +> val t = (Thm.term_of o the o (parse thy)) "6 + 5 * 4 + 3";
33.55 > const_in "sqrt" t;
33.56 val it = false : bool
33.57 *)
33.58 @@ -662,7 +662,7 @@
33.59 (arg1,arg2,range)
33.60 | dest_binop_typ _ = error "dest_binop_typ: not binary";
33.61 (* -----
33.62 -> val t = (term_of o the o (parse thy)) "#3^#4";
33.63 +> val t = (Thm.term_of o the o (parse thy)) "#3^#4";
33.64 > val hT = type_of (head_of t);
33.65 > dest_binop_typ hT;
33.66 val it = ("'a","nat","'a") : typ * typ * typ
33.67 @@ -767,7 +767,7 @@
33.68 | get ts (t1 $ t2) = (get ts t1) @ (get ts t2)
33.69 in distinct (get [] t) end;
33.70 (*
33.71 -val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
33.72 +val t = (Thm.term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
33.73 get_types t;
33.74 *)
33.75
33.76 @@ -793,17 +793,17 @@
33.77 Abs(s,T, set_types al body)))
33.78 | set_types al (t1 $ t2) = (set_types al t1) $ (set_types al t2);
33.79 (*
33.80 -val t = (term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
33.81 +val t = (Thm.term_of o the o (parse thy)) "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
33.82 val al = get_types t;
33.83
33.84 -val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
33.85 +val t = (Thm.term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
33.86 atomty t; (* 'a *)
33.87 val t' = set_types al t;
33.88 atomty t'; (*real*)
33.89 (Thm.global_cterm_of thy) t';
33.90 val it = "x = #0 + #-1 * #-4" : cterm
33.91
33.92 -val t = (term_of o the o (parse thy))
33.93 +val t = (Thm.term_of o the o (parse thy))
33.94 "#5 * x + x ^^^ #2 = (#2 + x) ^^^ #2";
33.95 atomty t;
33.96 val t' = set_types al t;
33.97 @@ -865,7 +865,7 @@
33.98 \ (s_1::bool list)=(SubProblem(DiffApp_,[univar,equation],[no_met])\
33.99 \ [BOOL e_1, REAL v_1])\
33.100 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
33.101 -> val ttt = (term_of o the o (parse thy)) scr;
33.102 +> val ttt = (Thm.term_of o the o (parse thy)) scr;
33.103 > tracing(term2str ttt);
33.104 > atomt ttt;
33.105 *** -------------
33.106 @@ -1059,7 +1059,7 @@
33.107 (*2002 fun parse thy str =
33.108 (let
33.109 val sgn = sign_of thy;
33.110 - val t = (typ_a2real o app_num_tr'1 o term_of)
33.111 + val t = (typ_a2real o app_num_tr'1 o Thm.term_of)
33.112 (read_cterm sgn (str,(TVar(("DUMMY",0),[]))));
33.113 in SOME (Thm.global_cterm_of sgn t) end) (*FIXXXXME 10.8.02: return term !!!*)
33.114 handle _ => NONE;*)
33.115 @@ -1074,14 +1074,14 @@
33.116 handle _ => NONE;
33.117 (*
33.118 > val (SOME ct) = parse thy "(-#5)^^^#3";
33.119 -> atomty (term_of ct);
33.120 +> atomty (Thm.term_of ct);
33.121 *** -------------
33.122 *** Const ( Nat.op ^, ['a, nat] => 'a)
33.123 *** Const ( uminus, 'a => 'a)
33.124 *** Free ( #5, 'a)
33.125 *** Free ( #3, nat)
33.126 > val (SOME ct) = parse thy "R=R";
33.127 -> atomty (term_of ct);
33.128 +> atomty (Thm.term_of ct);
33.129 *** -------------
33.130 *** Const ( op =, [real, real] => bool)
33.131 *** Free ( R, real)
33.132 @@ -1106,12 +1106,12 @@
33.133 |> typ_a2real; (*TODO drop*)
33.134
33.135 (*version for testing local to theories*)
33.136 -fun str2term_ thy str = (term_of o the o (parse thy)) str;
33.137 +fun str2term_ thy str = (Thm.term_of o the o (parse thy)) str;
33.138 (*WN110520
33.139 -fun str2term str = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) str;*)
33.140 +fun str2term str = (Thm.term_of o the o (parse (Thy_Info.get_theory "Isac"))) str;*)
33.141 fun str2term str = parse_patt (Thy_Info.get_theory "Isac") str
33.142 fun strs2terms ss = map str2term ss;
33.143 -fun str2termN str = (term_of o the o (parseN (Thy_Info.get_theory "Isac"))) str;
33.144 +fun str2termN str = (Thm.term_of o the o (parseN (Thy_Info.get_theory "Isac"))) str;
33.145
33.146 (*+ makes a substitution from the output of Pattern.match +*)
33.147 (*fun mk_subs ((id, _):indexname, t:term) = (Free (id,type_of t), t);*)
34.1 --- a/src/Tools/isac/library.sml Mon Dec 07 10:52:07 2015 +0100
34.2 +++ b/src/Tools/isac/library.sml Mon Dec 07 11:25:02 2015 +0100
34.3 @@ -254,7 +254,7 @@
34.4 | con ss _ = ss
34.5 in map strip_thy ((distinct o (con [])) t) end;
34.6 (*
34.7 -> val t = (term_of o the o (parse thy))
34.8 +> val t = (Thm.term_of o the o (parse thy))
34.9 "solve_univar (R, [univar, equation], no_met) (a = b + #1) a";
34.10 > ids_of t;
34.11 ["solve'_univar","Product_Type.Pair","R","Cons","univar","equation","Nil",...]*)
35.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Mon Dec 07 10:52:07 2015 +0100
35.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Mon Dec 07 11:25:02 2015 +0100
35.3 @@ -914,7 +914,7 @@
35.4 fun posformheads2xml j [] = ("":xml)
35.5 | posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs;
35.6
35.7 -val e_pblterm = (term_of o the o (parse @{theory Script}))
35.8 +val e_pblterm = (Thm.term_of o the o (parse @{theory Script}))
35.9 ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
35.10
35.11 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)