1.1 --- a/src/Tools/isac/Interpret/script.sml Mon Dec 07 10:52:07 2015 +0100
1.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Dec 07 11:25:02 2015 +0100
1.3 @@ -115,14 +115,14 @@
1.4 | go (R::p) (t1 $ t2) = go p t2
1.5 | go l _ = error ("go: no "^(loc_2str l));
1.6 (*
1.7 -> val t = (term_of o the o (parse thy)) "a+b";
1.8 +> val t = (Thm.term_of o the o (parse thy)) "a+b";
1.9 val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
1.10 > val plus_a = go [L] t;
1.11 > val b = go [R] t;
1.12 > val plus = go [L,L] t;
1.13 > val a = go [L,R] t;
1.14
1.15 -> val t = (term_of o the o (parse thy)) "a+b+c";
1.16 +> val t = (Thm.term_of o the o (parse thy)) "a+b+c";
1.17 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
1.18 > val pl_pl_a_b = go [L] t;
1.19 > val c = go [R] t;
1.20 @@ -148,7 +148,7 @@
1.21 NONE => get (l@[R]) test t2
1.22 | SOME (l',t') => SOME (l',t');
1.23 (*18.6.00
1.24 -> val sss = ((term_of o the o (parse thy))
1.25 +> val sss = ((Thm.term_of o the o (parse thy))
1.26 "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
1.27 \ (let e_ = Try (Rewrite square_equation_left True eq_) \
1.28 \ in [e_])");
1.29 @@ -225,10 +225,10 @@
1.30 | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term
1.31 | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
1.32 | itr_arg thy t = error ("itr_arg not impl. for " ^ term_to_string'' thy t);
1.33 -(* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
1.34 +(* val t = (Thm.term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
1.35 > itr_arg "Script" t;
1.36 val it = Free ("e_","RealDef.real") : term
1.37 -> val t = (term_of o the o (parse thy))"xxx";
1.38 +> val t = (Thm.term_of o the o (parse thy))"xxx";
1.39 > itr_arg "Script" t;
1.40 *** itr_arg not impl. for xxx
1.41 uncaught exception ERROR
1.42 @@ -261,13 +261,13 @@
1.43
1.44 (*get the _result_-type of a description*)
1.45 fun dsc_valT (Const (_,(Type (_,[_,T])))) = (strip_thy o typ_str) T;
1.46 -(*> val t = (term_of o the o (parse thy)) "equality";
1.47 +(*> val t = (Thm.term_of o the o (parse thy)) "equality";
1.48 > val T = type_of t;
1.49 val T = "bool => Tools.una" : typ
1.50 > val dsc = dsc_valT t;
1.51 val dsc = "una" : string
1.52
1.53 -> val t = (term_of o the o (parse thy)) "fixedValues";
1.54 +> val t = (Thm.term_of o the o (parse thy)) "fixedValues";
1.55 > val T = type_of t;
1.56 val T = "bool List.list => Tools.nam" : typ
1.57 > val dsc = dsc_valT t;
1.58 @@ -330,7 +330,7 @@
1.59
1.60 (*detour necessary, because generate1 delivers a string-result*)
1.61 fun mout2term thy (Form' (FormKF (_,_,_,_,res))) =
1.62 - (term_of o the o (parse (assoc_thy thy))) res
1.63 + (Thm.term_of o the o (parse (assoc_thy thy))) res
1.64 | mout2term thy (Form' (PpcKF _)) = e_term;(*3.8.01: res of subpbl
1.65 at time of detection in script*)
1.66
1.67 @@ -426,10 +426,10 @@
1.68 fun list_of_consts (Const ("List.list.Cons",_) $ _ $ _) = true
1.69 | list_of_consts (Const ("List.list.Nil",_)) = true
1.70 | list_of_consts _ = false;
1.71 -(*val ttt = (term_of o the o (parse thy)) "[x=#1,x=#2,x=#3]";
1.72 +(*val ttt = (Thm.term_of o the o (parse thy)) "[x=#1,x=#2,x=#3]";
1.73 > list_of_consts ttt;
1.74 val it = true : bool
1.75 -> val ttt = (term_of o the o (parse thy)) "[]";
1.76 +> val ttt = (Thm.term_of o the o (parse thy)) "[]";
1.77 > list_of_consts ttt;
1.78 val it = true : bool*)
1.79
1.80 @@ -579,7 +579,7 @@
1.81
1.82 | assod pt _ (m as Tac_ (thy,f,id,f')) (Const ("Script.Tac",_) $ Free (id',_)) =
1.83 if id = id'
1.84 - then Ass (m, ((term_of o the o (parse thy)) f'))
1.85 + then Ass (m, ((Thm.term_of o the o (parse thy)) f'))
1.86 else NotAss
1.87
1.88 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
1.89 @@ -676,14 +676,14 @@
1.90 unly needed --- **)
1.91
1.92 val idT = Type ("Script.ID",[]);
1.93 -(*val tt = (term_of o the o (parse thy)) "square_equation_left::ID";
1.94 +(*val tt = (Thm.term_of o the o (parse thy)) "square_equation_left::ID";
1.95 type_of tt = idT;
1.96 val it = true : bool
1.97 *)
1.98
1.99 fun make_rule thy t =
1.100 let val ct = Thm.global_cterm_of thy (Trueprop $ t)
1.101 - in Thm (term_to_string''' thy (term_of ct), Thm.make_thm ct) end;
1.102 + in Thm (term_to_string''' thy (Thm.term_of ct), Thm.make_thm ct) end;
1.103
1.104 (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
1.105 *)
1.106 @@ -709,7 +709,7 @@
1.107 val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
1.108 ML> subs;
1.109 val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
1.110 -> val tt = (term_of o the o (parse thy))
1.111 +> val tt = (Thm.term_of o the o (parse thy))
1.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))";
1.113 > atomty tt;
1.114 ML> tracing (term2str tt);
1.115 @@ -722,14 +722,14 @@
1.116
1.117
1.118 (*Fehlersuche 1-2Monate vor 4.01:*)
1.119 -> val tt = (term_of o the o (parse thy))
1.120 +> val tt = (Thm.term_of o the o (parse thy))
1.121 "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";
1.122 > atomty tt;
1.123
1.124 -> val f = (term_of o the o (parse thy)) "x=#1+#2";
1.125 -> val f' = (term_of o the o (parse thy)) "x=#3";
1.126 -> val subs = [((term_of o the o (parse thy)) "bdv",
1.127 - (term_of o the o (parse thy)) "x")];
1.128 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
1.129 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
1.130 +> val subs = [((Thm.term_of o the o (parse thy)) "bdv",
1.131 + (Thm.term_of o the o (parse thy)) "x")];
1.132 > val sT = (type_of o fst o hd) subs;
1.133 > val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
1.134 (map HOLogic.mk_prod subs);
1.135 @@ -750,11 +750,11 @@
1.136 $ Free (thmID,idT) $ b $ f;
1.137 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.138 (*
1.139 -> val tt = (term_of o the o (parse thy)) (*____ ____..test*)
1.140 +> val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
1.141 "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";
1.142
1.143 -> val f = (term_of o the o (parse thy)) "x=#1+#2";
1.144 -> val f' = (term_of o the o (parse thy)) "x=#3";
1.145 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
1.146 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
1.147 > val Thm (id,thm) =
1.148 rep_tac_ (Rewrite'
1.149 ("Script","tless_true","eval_rls",false,
1.150 @@ -796,12 +796,12 @@
1.151 val t = HOLogic.mk_eq (lhs,f');
1.152 make_rule thy t;
1.153 --------------------------------------------------
1.154 -val lll = (term_of o the o (parse thy))
1.155 +val lll = (Thm.term_of o the o (parse thy))
1.156 "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
1.157
1.158 --------------------------------------------------
1.159 -> val f = (term_of o the o (parse thy)) "x=#1+#2";
1.160 -> val f' = (term_of o the o (parse thy)) "x=#3";
1.161 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
1.162 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
1.163 > val Thm (id,thm) =
1.164 rep_tac_ (Rewrite_Set'
1.165 ("Script",false,"SqRoot_simplify",f,(f',[])));
1.166 @@ -814,7 +814,7 @@
1.167 $ Free (op_,idT) $ f
1.168 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.169 (*
1.170 -> val lhs'=(term_of o the o (parse thy))"Calculate plus (#1+#2)";
1.171 +> val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";
1.172 ... test-root-equ.sml: calculate ...
1.173 > val Appl m'=applicable_in p pt (Calculate "PLUS");
1.174 > val (lhs,_)=tac_2etac m';