1.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Mon Dec 07 11:32:12 2015 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Mon Dec 07 14:10:59 2015 +0100
1.3 @@ -35,7 +35,7 @@
1.4 text{*Apply the Method to an expression.*}
1.5
1.6 ML{*
1.7 - val input = term_of (the (parse thy "get_denominator ((a + b) / c)"));
1.8 + val input = Thm.term_of (the (parse thy "get_denominator ((a + b) / c)"));
1.9 val SOME (_, output) = eval_get_denominator "" 0 input thy;
1.10 *}
1.11
2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Dec 07 11:32:12 2015 +0100
2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Dec 07 14:10:59 2015 +0100
2.3 @@ -1076,7 +1076,7 @@
2.4 " in X)";
2.5
2.6 parse thy str;
2.7 - val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.8 + val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
2.9 atomty sc;
2.10 *}
2.11
3.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Dec 07 11:32:12 2015 +0100
3.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Dec 07 14:10:59 2015 +0100
3.3 @@ -88,7 +88,7 @@
3.4 will disappear), which does not encode numerals as binary numbers:
3.5 *}
3.6 ML {* val SOME t = parse @{theory "Isac"} "a + b * 3";
3.7 - atomwy (term_of t);
3.8 + atomwy (Thm.term_of t);
3.9 *}
3.10 text {* From the above we see: the internal representation of a term contains
3.11 all the knowledge it is built from, see
4.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Mon Dec 07 11:32:12 2015 +0100
4.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Mon Dec 07 14:10:59 2015 +0100
4.3 @@ -39,7 +39,7 @@
4.4 *}
4.5 text {* ... and let us differentiate the term t: *}
4.6 ML {*
4.7 -val t = (term_of o the o (parse thy)) "d_d x (x^^^2 + x + y)";
4.8 +val t = (Thm.term_of o the o (parse thy)) "d_d x (x^^^2 + x + y)";
4.9
4.10 val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
4.11 val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
4.12 @@ -78,10 +78,10 @@
4.13 text {* We have already seen conditional rewriting above when we used the rule
4.14 diff_const; let us try: *}
4.15 ML {*
4.16 -val t1 = (term_of o the o (parse thy)) "d_d x (a*BC*x*z)";
4.17 +val t1 = (Thm.term_of o the o (parse thy)) "d_d x (a*BC*x*z)";
4.18 rewrite_inst_ thy ro er true inst diff_const t1;
4.19
4.20 -val t2 = (term_of o the o (parse thy)) "d_d x (a*BC*y*z)";
4.21 +val t2 = (Thm.term_of o the o (parse thy)) "d_d x (a*BC*y*z)";
4.22 rewrite_inst_ thy ro er true inst diff_const t2;
4.23 *}
4.24 text {* For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false,
4.25 @@ -96,7 +96,7 @@
4.26 *}
4.27 ML {*
4.28 (*show_brackets := true; TODO*)
4.29 -val t0 = (term_of o the o (parse thy)) "2*a + 3*b + 4*a"; term2str t0;
4.30 +val t0 = (Thm.term_of o the o (parse thy)) "2*a + 3*b + 4*a"; term2str t0;
4.31 (*show_brackets := false;*)
4.32 *}
4.33 text {* Now we want to bring 4*a close to 2*a in order to get 6*a:
4.34 @@ -145,11 +145,11 @@
4.35 *}
4.36 ML {*
4.37 (*show_brackets := false; TODO*)
4.38 -val t1 = (term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)";
4.39 +val t1 = (Thm.term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)";
4.40 val SOME (t, _) = rewrite_set_ thy true make_polynomial t1; term2str t;
4.41 *}
4.42 ML {*
4.43 -val t2 = (term_of o the o (parse thy))
4.44 +val t2 = (Thm.term_of o the o (parse thy))
4.45 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))";
4.46 val SOME (t, _) = rewrite_set_ thy true norm_Rational t2; term2str t;
4.47 *}
4.48 @@ -185,7 +185,7 @@
4.49
4.50 subsection {* What already works *}
4.51 ML {*
4.52 -val t2 = (term_of o the o (parse thy))
4.53 +val t2 = (Thm.term_of o the o (parse thy))
4.54 "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
4.55 val SOME (t, _) = rewrite_set_ thy true rls_p_33 t2; term2str t;
4.56 *}
4.57 @@ -225,7 +225,7 @@
4.58
4.59 subsection {* This does not yet work *}
4.60 ML {*
4.61 -val t = (term_of o the o (parse thy))
4.62 +val t = (Thm.term_of o the o (parse thy))
4.63 "(2*a - 5*b) * (2*a + 5*b)";
4.64 rewrite_set_ thy true rls_p_33 t; term2str t;
4.65 *}
5.1 --- a/test/Tools/isac/Interpret/calchead.sml Mon Dec 07 11:32:12 2015 +0100
5.2 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Dec 07 14:10:59 2015 +0100
5.3 @@ -406,10 +406,10 @@
5.4 ============ inhibit exn AK110726 ==============================================*)
5.5 "--------------------------------step through code mtc---";
5.6 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
5.7 -cterm_of;
5.8 +Thm.global_cterm_of;
5.9 val ttt = (dsc $ var);
5.10 (*============ inhibit exn AK110726 ==============================================
5.11 -cterm_of thy (dsc $ var);
5.12 +Thm.global_cterm_of thy (dsc $ var);
5.13 ============ inhibit exn AK110726 ==============================================*)
5.14
5.15 "-------------------------------------step through end---";
5.16 @@ -497,10 +497,10 @@
5.17 -------------------------------------------------------------------*)
5.18 "--------------------------------step through code mtc---";
5.19 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
5.20 -cterm_of;
5.21 +Thm.global_cterm_of;
5.22 val ttt = (dsc $ var);
5.23 (*============ inhibit exn AK110726 ==============================================
5.24 -cterm_of thy (dsc $ var);
5.25 +Thm.global_cterm_of thy (dsc $ var);
5.26 -------------------------------------------------------------------*)
5.27 "-------------------------------------step through end---";
5.28
5.29 @@ -554,7 +554,7 @@
5.30 "--------------------------------step through code mtc---";
5.31 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
5.32 val ttt = (dsc $ var);
5.33 -cterm_of thy (dsc $ var);
5.34 +Thm.global_cterm_of thy (dsc $ var);
5.35 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
5.36
5.37 "-d2-----------------------------------------------------";
5.38 @@ -567,7 +567,7 @@
5.39 "--------------------------------step through code mtc---";
5.40 val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a);
5.41 val ttt = (dsc $ var);
5.42 -cterm_of thy (dsc $ var);
5.43 +Thm.global_cterm_of thy (dsc $ var);
5.44 val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori);
5.45 "-d3-----------------------------------------------------";
5.46 pbt = []; (*true, base case*)
6.1 --- a/test/Tools/isac/Interpret/inform.sml Mon Dec 07 11:32:12 2015 +0100
6.2 +++ b/test/Tools/isac/Interpret/inform.sml Mon Dec 07 14:10:59 2015 +0100
6.3 @@ -1018,7 +1018,7 @@
6.4 "~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
6.5 (cs', (encode ifo));
6.6 val SOME f_in = parse (assoc_thy "Isac") istr
6.7 -val f_in = term_of f_in
6.8 +val f_in = Thm.term_of f_in
6.9 val pos_pred = lev_back' pos
6.10 (* f_pred ---"step pos cs"---> f_succ in appendFormula
6.11 TODO.WN120517: one starting point for redesign of pos' *)
7.1 --- a/test/Tools/isac/Interpret/mathengine.sml Mon Dec 07 11:32:12 2015 +0100
7.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Mon Dec 07 14:10:59 2015 +0100
7.3 @@ -719,7 +719,7 @@
7.4 "~~~~~ fun inform, args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
7.5 (cs', (encode ifo));
7.6 val SOME f_in = parse (assoc_thy "Isac") istr
7.7 - val f_in = term_of f_in
7.8 + val f_in = Thm.term_of f_in
7.9 val f_succ = get_curr_formula (pt, pos);
7.10 f_succ = f_in = false;
7.11 val NONE = cas_input f_in
8.1 --- a/test/Tools/isac/Interpret/ptyps.sml Mon Dec 07 11:32:12 2015 +0100
8.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Mon Dec 07 14:10:59 2015 +0100
8.3 @@ -26,20 +26,20 @@
8.4 val ctxt = Proof_Context.init_global @{theory "Isac"};
8.5
8.6 (*case 1: no refinement *)
8.7 -val (d1,ts1) = split_dts ((term_of o the o (parse thy)) "fixedValues [aaa = 0]");
8.8 -val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "errorBound (ddd = 0)");
8.9 +val (d1,ts1) = split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]");
8.10 +val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)");
8.11 val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: ori list;
8.12
8.13 (*case 2: refined to pbt without children *)
8.14 -val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "relations [aaa333]");
8.15 +val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]");
8.16 val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
8.17
8.18 (*case 3: refined to pbt with children *)
8.19 -val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "valuesFor [aaa222]");
8.20 +val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]");
8.21 val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list;
8.22
8.23 (*case 4: refined to children (without child)*)
8.24 -val (d3,ts3) = split_dts ((term_of o the o (parse thy)) "boundVariable aaa222yyy");
8.25 +val (d3,ts3) = split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy");
8.26 val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:ori list;
8.27
8.28 (*=================================================================
9.1 --- a/test/Tools/isac/Interpret/script.sml Mon Dec 07 11:32:12 2015 +0100
9.2 +++ b/test/Tools/isac/Interpret/script.sml Mon Dec 07 14:10:59 2015 +0100
9.3 @@ -33,7 +33,7 @@
9.4 " (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^
9.5 " in True)";
9.6
9.7 -val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
9.8 +val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
9.9
9.10 val str = (*#2#*)
9.11 "Script BiegelinieScript " ^
9.12 @@ -74,7 +74,7 @@
9.13 " in True)"
9.14 ;
9.15
9.16 -val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
9.17 +val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
9.18 atomty sc';
9.19
9.20 val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
9.21 @@ -98,7 +98,7 @@
9.22 " M1__M1 = Substitute [e1__e1] M1__M1 " ^
9.23 " in True)"
9.24 ;
9.25 -val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
9.26 +val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
9.27 atomty sc';
9.28
9.29 val str = (*Substitute @@ Substitute does NOT work???*)
10.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Mon Dec 07 11:32:12 2015 +0100
10.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Mon Dec 07 14:10:59 2015 +0100
10.3 @@ -47,7 +47,7 @@
10.4 " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
10.5 "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
10.6 ;
10.7 -val sc = ((inst_abs thy) o term_of o the o (parse @{theory Isac})) str;
10.8 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse @{theory Isac})) str;
10.9 writeln (term2str sc);
10.10
10.11 "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = ";
11.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Dec 07 11:32:12 2015 +0100
11.2 +++ b/test/Tools/isac/Knowledge/algein.sml Mon Dec 07 14:10:59 2015 +0100
11.3 @@ -29,7 +29,7 @@
11.4 \ (let t_t = (l_l = 1)\
11.5 \ in t_t)"
11.6 ;
11.7 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
11.8 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
11.9 atomty sc;
11.10 atomt sc;
11.11
12.1 --- a/test/Tools/isac/Knowledge/atools.sml Mon Dec 07 11:32:12 2015 +0100
12.2 +++ b/test/Tools/isac/Knowledge/atools.sml Mon Dec 07 14:10:59 2015 +0100
12.3 @@ -28,7 +28,7 @@
12.4 "----------- occurs_in -------------------------------------------";
12.5 "----------- occurs_in -------------------------------------------";
12.6 (*=========================================================================*)
12.7 -fun str2t str = (term_of o the o (parse thy)) str;
12.8 +fun str2t str = (Thm.term_of o the o (parse thy)) str;
12.9 fun term2s t = term_to_string''' thy t;
12.10 (*=========================================================================*)
12.11
12.12 @@ -139,14 +139,14 @@
12.13 "----------- Matthias Goldgruber 2003 rewrite orders ----";
12.14 "----------- Matthias Goldgruber 2003 rewrite orders ----";
12.15 (* MK die ersten Tests *)
12.16 - val substa = [(e_term, (term_of o the o (parse thy)) "a")];
12.17 - val substb = [(e_term, (term_of o the o (parse thy)) "b")];
12.18 - val substx = [(e_term, (term_of o the o (parse thy)) "x")];
12.19 + val substa = [(e_term, (Thm.term_of o the o (parse thy)) "a")];
12.20 + val substb = [(e_term, (Thm.term_of o the o (parse thy)) "b")];
12.21 + val substx = [(e_term, (Thm.term_of o the o (parse thy)) "x")];
12.22
12.23 - val x1 = (term_of o the o (parse thy)) "a + b + x";
12.24 - val x2 = (term_of o the o (parse thy)) "a + x + b";
12.25 - val x3 = (term_of o the o (parse thy)) "a + x + b";
12.26 - val x4 = (term_of o the o (parse thy)) "x + a + b";
12.27 + val x1 = (Thm.term_of o the o (parse thy)) "a + b + x";
12.28 + val x2 = (Thm.term_of o the o (parse thy)) "a + x + b";
12.29 + val x3 = (Thm.term_of o the o (parse thy)) "a + x + b";
12.30 + val x4 = (Thm.term_of o the o (parse thy)) "x + a + b";
12.31
12.32 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
12.33 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
12.34 @@ -157,22 +157,22 @@
12.35 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
12.36 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
12.37
12.38 - val aa = (term_of o the o (parse thy)) "-1 * a * x";
12.39 - val bb = (term_of o the o (parse thy)) "x^^^3";
12.40 + val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
12.41 + val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
12.42 ord_make_polynomial_in true thy substx (aa, bb);
12.43 true; (* => LESS *)
12.44
12.45 - val aa = (term_of o the o (parse thy)) "-1 * a * x";
12.46 - val bb = (term_of o the o (parse thy)) "x^^^3";
12.47 + val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x";
12.48 + val bb = (Thm.term_of o the o (parse thy)) "x^^^3";
12.49 ord_make_polynomial_in true thy substa (aa, bb);
12.50 false; (* => GREATER *)
12.51
12.52 (* und nach dem Re-engineering der Termorders in den 'rulesets'
12.53 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
12.54 - val bdv= (term_of o the o (parse thy)) "bdv";
12.55 - val x = (term_of o the o (parse thy)) "x";
12.56 - val a = (term_of o the o (parse thy)) "a";
12.57 - val b = (term_of o the o (parse thy)) "b";
12.58 + val bdv= (Thm.term_of o the o (parse thy)) "bdv";
12.59 + val x = (Thm.term_of o the o (parse thy)) "x";
12.60 + val a = (Thm.term_of o the o (parse thy)) "a";
12.61 + val b = (Thm.term_of o the o (parse thy)) "b";
12.62 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
12.63 if term2str t' = "b + x + a" then ()
12.64 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
12.65 @@ -184,7 +184,7 @@
12.66 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
12.67
12.68 val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
12.69 - val ppp = (term_of o the o (parse thy)) ppp';
12.70 + val ppp = (Thm.term_of o the o (parse thy)) ppp';
12.71 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
12.72 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
12.73 else error "termorder.sml diff.behav ord_make_polynomial_in #14";
12.74 @@ -194,7 +194,7 @@
12.75 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
12.76
12.77 val ttt' = "(3*x + 5)/18";
12.78 - val ttt = (term_of o the o (parse thy)) ttt';
12.79 + val ttt = (Thm.term_of o the o (parse thy)) ttt';
12.80 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
12.81 if term2str uuu = "(5 + 3 * x) / 18" then ()
12.82 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
12.83 @@ -213,7 +213,7 @@
12.84 -----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
12.85
12.86 (*Aufgabe zum Einstieg in die Arbeit...*)
12.87 - val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
12.88 + val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
12.89 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
12.90 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
12.91 term2str t;
12.92 @@ -243,9 +243,9 @@
12.93 *)
12.94
12.95 "------15.11.02 --------------------------";
12.96 - val t = (term_of o the o (parse thy)) "1 + a * x + b * x";
12.97 - val bdv = (term_of o the o (parse thy)) "bdv";
12.98 - val a = (term_of o the o (parse thy)) "a";
12.99 + val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x";
12.100 + val bdv = (Thm.term_of o the o (parse thy)) "bdv";
12.101 + val a = (Thm.term_of o the o (parse thy)) "a";
12.102
12.103 trace_rewrite := false;
12.104 (* Anwenden einer Regelmenge aus Termorder.ML: *)
12.105 @@ -257,7 +257,7 @@
12.106 term2str t;
12.107 "1 + b * x + x * a";
12.108
12.109 - val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
12.110 + val t = (Thm.term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
12.111 val SOME (t,_) =
12.112 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
12.113 term2str t;
12.114 @@ -266,7 +266,7 @@
12.115 term2str t;
12.116 "1 + (x + b * x) * a + a ^^^ 2";
12.117
12.118 - val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
12.119 + val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
12.120 val SOME (t,_) =
12.121 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
12.122 term2str t;
12.123 @@ -286,7 +286,7 @@
12.124 get_thm Termorder.thy "bdv_n_collect";
12.125 get_thm (theory "Isac") "bdv_n_collect";
12.126 *)
12.127 - val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
12.128 + val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
12.129 val SOME (t,_) =
12.130 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
12.131 term2str t;
12.132 @@ -295,16 +295,16 @@
12.133 term2str t;
12.134 "(7 + x) * a ^^^ 2";
12.135
12.136 - val t = (term_of o the o (parse Termorder.thy)) "Pi";
12.137 + val t = (Thm.term_of o the o (parse Termorder.thy)) "Pi";
12.138
12.139 - val t = (term_of o the o (parseold thy)) "7";
12.140 + val t = (Thm.term_of o the o (parseold thy)) "7";
12.141 ##################################################################################*)
12.142
12.143 "----------- fun eval_binop -----------------------------";
12.144 "----------- fun eval_binop -----------------------------";
12.145 "----------- fun eval_binop -----------------------------";
12.146 val (op_, ef) = the (assoc (calclist, "TIMES"));
12.147 -val t = (term_of o the o (parse thy)) "2 * 3";
12.148 +val t = (Thm.term_of o the o (parse thy)) "2 * 3";
12.149 (*val SOME (thmid,t') = *)get_pair thy op_ ef t;
12.150 ;
12.151 "~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
13.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Mon Dec 07 11:32:12 2015 +0100
13.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Mon Dec 07 14:10:59 2015 +0100
13.3 @@ -22,7 +22,7 @@
13.4
13.5 val thy = @{theory "Biegelinie"};
13.6 val ctxt = thy2ctxt' "Biegelinie";
13.7 -fun str2term str = (term_of o the o (parse thy)) str;
13.8 +fun str2term str = (Thm.term_of o the o (parse thy)) str;
13.9 fun term2s t = term_to_string'' "Biegelinie" t;
13.10 fun rewrit thm str =
13.11 fst (the (rewrite_ thy tless_true e_rls true thm str));
14.1 --- a/test/Tools/isac/Knowledge/diff.sml Mon Dec 07 11:32:12 2015 +0100
14.2 +++ b/test/Tools/isac/Knowledge/diff.sml Mon Dec 07 14:10:59 2015 +0100
14.3 @@ -301,7 +301,7 @@
14.4 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
14.5 \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')"
14.6 ;
14.7 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
14.8 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
14.9
14.10
14.11 "----------- diff_conv, sym_diff_conv -------------------";
15.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Dec 07 11:32:12 2015 +0100
15.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon Dec 07 14:10:59 2015 +0100
15.3 @@ -93,9 +93,9 @@
15.4 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
15.5
15.6 val SOME t = parse thy "solution LL";
15.7 -atomty (term_of t);
15.8 +atomty (Thm.term_of t);
15.9 val SOME t = parse thy "solution LL";
15.10 -atomty (term_of t);
15.11 +atomty (Thm.term_of t);
15.12
15.13 val t = str2term
15.14 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
15.15 @@ -449,7 +449,7 @@
15.16 *)
15.17 > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
15.18 val equalities_es_ = "equalities es_" : string
15.19 -> val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
15.20 +> val (dd, ii) = (split_did o Thm.term_of o the o (parse thy)) equalities_es_;
15.21 > show_types:=true; term2str ii; show_types:=false;
15.22 val it = "es_::bool list" : string
15.23 ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
16.1 --- a/test/Tools/isac/Knowledge/inssort.sml Mon Dec 07 11:32:12 2015 +0100
16.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Mon Dec 07 14:10:59 2015 +0100
16.3 @@ -117,11 +117,11 @@
16.4
16.5
16.6 (* ------- 17.6.00: mit kleinen problemen aufgegeben
16.7 -val scr=Prog ((term_of o the o (parse thy))
16.8 +val scr=Prog ((Thm.term_of o the o (parse thy))
16.9 "Script Sort (u_::'a list) = \
16.10 \ Rewrite_Set ins_sort False u_");
16.11
16.12 -val scr=Prog ((term_of o the o (parse thy))
16.13 +val scr=Prog ((Thm.term_of o the o (parse thy))
16.14 "Script Ins_sort (u_::real list) = \
16.15 \ (let u_ = Rewrite sort_def False u_; \
16.16 \ u_ = Rewrite foldr_rec False u_; \
16.17 @@ -155,7 +155,7 @@
16.18 \ u_ = u_ \
16.19 \ in u_)";
16.20
16.21 -atomty (term_of (the scr));
16.22 +atomty (Thm.term_of (the scr));
16.23
16.24 ------- *)
16.25 ============ inhibit exn =====================================================*)
17.1 --- a/test/Tools/isac/Knowledge/integrate.sml Mon Dec 07 11:32:12 2015 +0100
17.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon Dec 07 14:10:59 2015 +0100
17.3 @@ -327,9 +327,9 @@
17.4 With =[],
17.5 Relate=[]}:string ppc;
17.6 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
17.7 -val t1 = (term_of o hd) chkmodel;
17.8 -val t2 = (term_of o hd o tl) chkmodel;
17.9 -val t3 = (term_of o hd o tl o tl) chkmodel;
17.10 +val t1 = (Thm.term_of o hd) chkmodel;
17.11 +val t2 = (Thm.term_of o hd o tl) chkmodel;
17.12 +val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
17.13 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
17.14 | _ => error "integrate.sml: Integrate.antiDerivative ???";
17.15
17.16 @@ -339,9 +339,9 @@
17.17 With =[],
17.18 Relate=[]}:string ppc;
17.19 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
17.20 -val t1 = (term_of o hd) chkmodel;
17.21 -val t2 = (term_of o hd o tl) chkmodel;
17.22 -val t3 = (term_of o hd o tl o tl) chkmodel;
17.23 +val t1 = (Thm.term_of o hd) chkmodel;
17.24 +val t2 = (Thm.term_of o hd o tl) chkmodel;
17.25 +val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
17.26 case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
17.27 | _ => error "integrate.sml: Integrate.antiDerivativeName";
17.28
17.29 @@ -372,14 +372,14 @@
17.30 "Script IntegrationScript (f_f::real) (v_v::real) = \
17.31 \ (let t_t = Take (Integral f_f D v_v) \
17.32 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))";
17.33 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
17.34 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
17.35 atomty sc;
17.36
17.37 val str =
17.38 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
17.39 \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \
17.40 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_t)";
17.41 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
17.42 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
17.43 atomty sc;
17.44 show_mets();
17.45
18.1 --- a/test/Tools/isac/Knowledge/poly.sml Mon Dec 07 11:32:12 2015 +0100
18.2 +++ b/test/Tools/isac/Knowledge/poly.sml Mon Dec 07 14:10:59 2015 +0100
18.3 @@ -38,7 +38,7 @@
18.4 "-------- investigate (new 2002) uniary minus -----------";
18.5 "-------- investigate (new 2002) uniary minus -----------";
18.6 (*---------------------------------------------- vvvvvvvvvvvvvv -----------------------*)
18.7 -val t = (#prop o rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
18.8 +val t = (#prop o Thm.rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
18.9 atomty t;
18.10 (*
18.11 *** Const (HOL.Trueprop, bool => prop)
18.12 @@ -58,7 +58,7 @@
18.13 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
18.14
18.15 (*----------------------------------- vvvv --------------------------------------------*)
18.16 -val t = (term_of o the o (parse thy)) "-1";
18.17 +val t = (Thm.term_of o the o (parse thy)) "-1";
18.18 atomty t;
18.19 (*** -------------
18.20 *** Free ( -1, real) *)
18.21 @@ -66,7 +66,7 @@
18.22 Free ("-1", _) => ()
18.23 | _ => error "internal representation of \"-1\" changed";
18.24 (*----------------------------------- vvvvv -------------------------------------------*)
18.25 -val t = (term_of o the o (parse thy)) "- 1";
18.26 +val t = (Thm.term_of o the o (parse thy)) "- 1";
18.27 atomty t;
18.28 (*
18.29 ***
18.30 @@ -80,7 +80,7 @@
18.31 "======= these external values all have the same internal representation";
18.32 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
18.33 (*----------------------------------- vvvvv -------------------------------------------*)
18.34 -val t = (term_of o the o (parse thy)) "-x";
18.35 +val t = (Thm.term_of o the o (parse thy)) "-x";
18.36 atomty t;
18.37 (**** -------------
18.38 *** Free ( -x, real)*)
18.39 @@ -88,7 +88,7 @@
18.40 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
18.41 | _ => error "internal representation of \"-x\" changed";
18.42 (*----------------------------------- vvvvv -------------------------------------------*)
18.43 -val t = (term_of o the o (parse thy)) "- x";
18.44 +val t = (Thm.term_of o the o (parse thy)) "- x";
18.45 atomty t;
18.46 (**** -------------
18.47 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
18.48 @@ -96,7 +96,7 @@
18.49 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
18.50 | _ => error "internal representation of \"- x\" changed";
18.51 (*----------------------------------- vvvvvv ------------------------------------------*)
18.52 -val t = (term_of o the o (parse thy)) "-(x)";
18.53 +val t = (Thm.term_of o the o (parse thy)) "-(x)";
18.54 atomty t;
18.55 (**** -------------
18.56 *** Free ( -x, real)*)
18.57 @@ -338,7 +338,7 @@
18.58 if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()
18.59 else error "poly.sml: diff.behav. in make_polynomial 23";
18.60 "-----SPO ---";
18.61 -val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
18.62 +val t = (Thm.term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
18.63 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
18.64 if (term2str t) = "a ^^^ 4" then ()
18.65 else error "poly.sml: diff.behav. in make_polynomial 24";
19.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Mon Dec 07 11:32:12 2015 +0100
19.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Mon Dec 07 14:10:59 2015 +0100
19.3 @@ -35,54 +35,54 @@
19.4 trace_rewrite:=true;
19.5 trace_rewrite:=false;
19.6 *)
19.7 - val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
19.8 + val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
19.9 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
19.10 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
19.11 else error "polyeq.sml: diff.behav. in lhs";
19.12
19.13 - val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
19.14 + val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
19.15 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
19.16 if (term2str t) = "True" then ()
19.17 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
19.18
19.19 - val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
19.20 + val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
19.21 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
19.22 if (term2str t) = "False" then ()
19.23 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
19.24
19.25 - val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
19.26 + val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
19.27 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
19.28 if (term2str t) = "True" then ()
19.29 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
19.30
19.31 - val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
19.32 + val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
19.33 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
19.34 if (term2str t) = "True" then ()
19.35 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
19.36
19.37
19.38 - val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
19.39 + val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
19.40 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
19.41 if (term2str t) = "True" then ()
19.42 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
19.43
19.44 - val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
19.45 + val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
19.46 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
19.47 if (term2str t) = "True" then ()
19.48 else error "polyeq.sml: diff.behav. in has_degree_in_in";
19.49
19.50 - val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
19.51 + val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
19.52 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
19.53 if (term2str t) = "False" then ()
19.54 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
19.55
19.56 - val t4 = (term_of o the o (parse thy))
19.57 + val t4 = (Thm.term_of o the o (parse thy))
19.58 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
19.59 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
19.60 if (term2str t) = "False" then ()
19.61 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
19.62
19.63 - val t5 = (term_of o the o (parse thy))
19.64 + val t5 = (Thm.term_of o the o (parse thy))
19.65 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
19.66 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
19.67 if (term2str t) = "True" then ()
19.68 @@ -833,7 +833,7 @@
19.69 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
19.70 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
19.71 "---- test the erls ----";
19.72 - val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
19.73 + val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
19.74 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
19.75 val t' = term2str t;
19.76 (*if t'= "HOL.True" then ()
19.77 @@ -1146,14 +1146,14 @@
19.78 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(bdv,x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)
19.79 t |> term2str; t |> atomty;
19.80 val thm = num_str @{thm d2_prescind1};
19.81 -thm |> prop_of |> term2str; thm|> prop_of |> atomty;
19.82 +thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
19.83 val SOME (t', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t; term2str t';
19.84
19.85 (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(bdv,x)"],("d2_reduce_equation1",""))
19.86 --> x = 0 | -6 + 5 * x = 0*)
19.87 t' |> term2str; t' |> atomty;
19.88 val thm = num_str @{thm d2_reduce_equation1};
19.89 -thm |> prop_of |> term2str; thm|> prop_of |> atomty;
19.90 +thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty;
19.91 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t'; term2str t'';
19.92 (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
19.93 instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
20.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Dec 07 11:32:12 2015 +0100
20.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Dec 07 14:10:59 2015 +0100
20.3 @@ -238,7 +238,7 @@
20.4 \ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
20.5 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \
20.6 \ (Try (Rewrite_Set verschoenere False))) t_t)"
20.7 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
20.8 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
20.9 atomty sc;
20.10
20.11 "----------- me simplification.for_polynomials.with_minus";
20.12 @@ -344,7 +344,7 @@
20.13 \ in (Repeat((Try (Repeat (Calculate TIMES))) @@ \
20.14 \ (Try (Repeat (Calculate PLUS ))) @@ \
20.15 \ (Try (Repeat (Calculate MINUS))))) e_e)"
20.16 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
20.17 +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
20.18 atomty sc;
20.19
20.20 "----------- pbl polynom probe -----------------------------------";
21.1 --- a/test/Tools/isac/Knowledge/rateq.sml Mon Dec 07 11:32:12 2015 +0100
21.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Mon Dec 07 14:10:59 2015 +0100
21.3 @@ -19,22 +19,22 @@
21.4 "------------ pbl: rational, univariate, equation ----------------";
21.5 "------------ pbl: rational, univariate, equation ----------------";
21.6 "------------ pbl: rational, univariate, equation ----------------";
21.7 -val t = (term_of o the o (parse thy)) "(1/b+1/x=1) is_ratequation_in x";
21.8 +val t = (Thm.term_of o the o (parse thy)) "(1/b+1/x=1) is_ratequation_in x";
21.9 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
21.10 val result = term2str t_;
21.11 if result <> "True" then error "rateq.sml: new behaviour 1:" else ();
21.12
21.13 -val t = (term_of o the o (parse thy)) "(sqrt(x)=1) is_ratequation_in x";
21.14 +val t = (Thm.term_of o the o (parse thy)) "(sqrt(x)=1) is_ratequation_in x";
21.15 val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t;
21.16 val result = term2str t_;
21.17 if result <> "False" then error "rateq.sml: new behaviour 2:" else ();
21.18
21.19 -val t = (term_of o the o (parse thy)) "(x=-1) is_ratequation_in x";
21.20 +val t = (Thm.term_of o the o (parse thy)) "(x=-1) is_ratequation_in x";
21.21 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
21.22 val result = term2str t_;
21.23 if result <> "False" then error "rateq.sml: new behaviour 3:" else ();
21.24
21.25 -val t = (term_of o the o (parse thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
21.26 +val t = (Thm.term_of o the o (parse thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
21.27 val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t;
21.28 val result = term2str t_;
21.29 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
22.1 --- a/test/Tools/isac/Knowledge/rational-old.sml Mon Dec 07 11:32:12 2015 +0100
22.2 +++ b/test/Tools/isac/Knowledge/rational-old.sml Mon Dec 07 14:10:59 2015 +0100
22.3 @@ -175,18 +175,18 @@
22.4
22.5 (*
22.6 print("***** TERM2POLY-TESTS *****\n");
22.7 -val t0 = (term_of o the o (parse thy)) "3 * 4";
22.8 -val t1 = (term_of o the o (parse thy)) "27";
22.9 -val t11= (term_of o the o (parse thy)) "27 * c";
22.10 -val t2 = (term_of o the o (parse thy)) "b";
22.11 -val t23= (term_of o the o (parse thy)) "c^^^7";
22.12 -val t24= (term_of o the o (parse thy)) "5 * c^^^7";
22.13 -val t26= (term_of o the o (parse thy)) "a * b";
22.14 -val t3 = (term_of o the o (parse thy)) "2 + a";
22.15 -val t4 = (term_of o the o (parse thy)) "b + a";
22.16 -val t5 = (term_of o the o (parse thy)) "2 + a^^^3";*)
22.17 -val t6 = (term_of o the o (parse thy)) "5*a^^^2*b^^^3*c+4*a^^^4*b+2*a*c";
22.18 -val t7 = (term_of o the o (parse thy)) "a-b";
22.19 +val t0 = (Thm.term_of o the o (parse thy)) "3 * 4";
22.20 +val t1 = (Thm.term_of o the o (parse thy)) "27";
22.21 +val t11= (Thm.term_of o the o (parse thy)) "27 * c";
22.22 +val t2 = (Thm.term_of o the o (parse thy)) "b";
22.23 +val t23= (Thm.term_of o the o (parse thy)) "c^^^7";
22.24 +val t24= (Thm.term_of o the o (parse thy)) "5 * c^^^7";
22.25 +val t26= (Thm.term_of o the o (parse thy)) "a * b";
22.26 +val t3 = (Thm.term_of o the o (parse thy)) "2 + a";
22.27 +val t4 = (Thm.term_of o the o (parse thy)) "b + a";
22.28 +val t5 = (Thm.term_of o the o (parse thy)) "2 + a^^^3";*)
22.29 +val t6 = (Thm.term_of o the o (parse thy)) "5*a^^^2*b^^^3*c+4*a^^^4*b+2*a*c";
22.30 +val t7 = (Thm.term_of o the o (parse thy)) "a-b";
22.31 (*
22.32 (the o term2poly) t0;
22.33 (the o term2poly) t1;
22.34 @@ -204,28 +204,28 @@
22.35
22.36 print("\n\n***** STEP_CANCEL_TESTS: *****\n");
22.37 (*
22.38 -val term2 = (term_of o the o (parse thy)) " (9 * a^^^2 * b) /// (6 * a * c)";
22.39 +val term2 = (Thm.term_of o the o (parse thy)) " (9 * a^^^2 * b) /// (6 * a * c)";
22.40 val div2 = step_cancel term2;
22.41 atomt div2;
22.42 *)
22.43
22.44 -val term1 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) /// a";
22.45 +val term1 = (Thm.term_of o the o (parse thy)) "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) /// a";
22.46 val div1 = step_cancel term1;
22.47 -(*if div1 = (term_of o the o (parse thy)) "((10 * a * b * c + 14 * b + 3 * c + 20 * b^^^2 * c) * a) /// (1 * a)" then () else raise error ("Test failed");*)
22.48 +(*if div1 = (Thm.term_of o the o (parse thy)) "((10 * a * b * c + 14 * b + 3 * c + 20 * b^^^2 * c) * a) /// (1 * a)" then () else raise error ("Test failed");*)
22.49
22.50 -val term2 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) /// (5 * a * b * c + 7 * a^^^2 * b * c) ";
22.51 +val term2 = (Thm.term_of o the o (parse thy)) "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) /// (5 * a * b * c + 7 * a^^^2 * b * c) ";
22.52 val div2 = step_cancel term2;
22.53 (*if div2 = ([(10,[1,1,1]),(20,[0,2,1]),(14,[0,1,0]),(3,[0,0,1])],[(1,[1,0,0])],[(7,[1,1,1]),(5,[0,1,1])]) then () else raise error ("Test failed");*)
22.54
22.55
22.56 -val term3 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c) /// (1 * x * y * z) ";
22.57 +val term3 = (Thm.term_of o the o (parse thy)) "(10 * a^^^2 * b * c) /// (1 * x * y * z) ";
22.58 val div3 = step_cancel term3;
22.59
22.60
22.61
22.62 -(*val mul1=(term_of o the o (parse thy)) "(5*a*b*c+4*a*b+2*a*c)";
22.63 -val mul2=(the (term2poly((term_of o the o (parse thy)) "13*a^^^2*b*c+7*a*b-19*a*b*c^^^2")));
22.64 -val mul3=(the (term2poly((term_of o the o (parse thy)) "6*a*b^^^2-13*a^^^2*b^^^2*c^^^2+21*a^^^2*b*c")));
22.65 +(*val mul1=(Thm.term_of o the o (parse thy)) "(5*a*b*c+4*a*b+2*a*c)";
22.66 +val mul2=(the (term2poly((Thm.term_of o the o (parse thy)) "13*a^^^2*b*c+7*a*b-19*a*b*c^^^2")));
22.67 +val mul3=(the (term2poly((Thm.term_of o the o (parse thy)) "6*a*b^^^2-13*a^^^2*b^^^2*c^^^2+21*a^^^2*b*c")));
22.68 val t1=mv_mul(mul1,mul2,LEX_);
22.69 val t2=mv_mul(mul3,mul2,LEX_);
22.70 val div3=step_cancel t1 t2;
22.71 @@ -237,7 +237,7 @@
22.72
22.73 val thy = Rational.thy;
22.74 val rls = Prls {func=cancel};
22.75 -val t = (term_of o the o (parse thy))
22.76 +val t = (Thm.term_of o the o (parse thy))
22.77 "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2)";
22.78 val (t,asm) = the (rewrite_set_ thy eval_rls false rls t);
22.79
22.80 @@ -261,9 +261,9 @@
22.81 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t');
22.82
22.83 (*
22.84 -val term2 = (term_of o the o (parse thy)) "(a^^^2 * b + 2 * a * b + b ) /// ( a^^^2 - 1 )";
22.85 +val term2 = (Thm.term_of o the o (parse thy)) "(a^^^2 * b + 2 * a * b + b ) /// ( a^^^2 - 1 )";
22.86 val div2 = direct_cancel term2;
22.87 -val t = (term_of o the o (parse thy)) "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2) = 0";*)
22.88 +val t = (Thm.term_of o the o (parse thy)) "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2) = 0";*)
22.89
22.90
22.91
22.92 @@ -291,7 +291,7 @@
22.93 val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
22.94 val e186c = (the (rewrite_set thy' "rational_erls" false rls' e186c'))
22.95 handle e => OldGoals.print_exn e;
22.96 -val t = (term_of o the o (parse thy)) e186c';
22.97 +val t = (Thm.term_of o the o (parse thy)) e186c';
22.98 atomt t;
22.99
22.100 print("\n\nexample 187:\n");
22.101 @@ -600,7 +600,7 @@
22.102
22.103
22.104 (*
22.105 - val t = (term_of o the o (parse thy))
22.106 + val t = (Thm.term_of o the o (parse thy))
22.107 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
22.108 val SOME (t',_) = factor_expanded_ thy t;
22.109 term2str t';
22.110 @@ -616,7 +616,7 @@
22.111 the 'reverse-ruleset' cancel*)
22.112
22.113 (*the term for which reverse rewriting is demonstrated*)
22.114 - val t = (term_of o the o (parse thy))
22.115 + val t = (Thm.term_of o the o (parse thy))
22.116 "(9 - x ^^^ 2) / (9 + 6 * x + x ^^^ 2)";
22.117 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
22.118 next_rule=nex,normal_form=nor,...},...} = cancel;
22.119 @@ -677,7 +677,7 @@
22.120 (*WN.11.9.02: the 'reverse-ruleset' cancel*)
22.121
22.122 (*the term for which reverse rewriting is demonstrated*)
22.123 - val t = (term_of o the o (parse thy))
22.124 + val t = (Thm.term_of o the o (parse thy))
22.125 "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
22.126 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
22.127 next_rule=nex,normal_form=nor,...},...} = cancel;
22.128 @@ -731,8 +731,8 @@
22.129 OK Thm ("real_mult_div_cancel2","?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n")]
22.130 -------- revset ----------------------------------------------------
22.131
22.132 - val t = (term_of o the o (parse thy)) "(-6) * x";
22.133 - val t = (term_of o the o (parse thy))
22.134 + val t = (Thm.term_of o the o (parse thy)) "(-6) * x";
22.135 + val t = (Thm.term_of o the o (parse thy))
22.136 "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
22.137 val thm = (mk_thm thy "(-6) * x = 2 * ((-3) * x)")
22.138 handle e => OldGoals.print_exn e;
22.139 @@ -744,38 +744,38 @@
22.140
22.141 (* SK: Testbeispiele --- WN kopiert Rational.ML -> rational.sml-----
22.142
22.143 -val t1 = (term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
22.144 +val t1 = (Thm.term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
22.145 val SOME (t1',rest)= cancel_ thy t1;
22.146 val SOME (t1'',_)= factor_out_gcd_ thy t1;
22.147 print(term2str t1'^" + Einschr\"ankung: "^term2str (hd(rest)));
22.148 term2str t1'';
22.149
22.150 -val t1 = (term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
22.151 +val t1 = (Thm.term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
22.152 val SOME (t1',_)= cancel_ thy t1;
22.153 val SOME (t1'',_)= factor_expanded_ thy t1;
22.154 term2str t1';
22.155 term2str t1'';
22.156
22.157 -val t2 = (term_of o the o (parse thy)) "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
22.158 +val t2 = (Thm.term_of o the o (parse thy)) "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
22.159 val SOME (t2',_) = add_fractions_ thy t2;
22.160 val SOME (t2'',_) = common_nominators_ thy t2;
22.161 term2str t2';
22.162 term2str t2'';
22.163
22.164 -val t2 = (term_of o the o (parse thy)) "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
22.165 +val t2 = (Thm.term_of o the o (parse thy)) "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
22.166 val SOME (t2',_) = add_expanded_frac_ thy t2;
22.167 val SOME (t2'',_) = common_expanded_nom_ thy t2;
22.168 term2str t2';
22.169 term2str t2'';
22.170
22.171
22.172 -val t3 = (term_of o the o (parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
22.173 +val t3 = (Thm.term_of o the o (parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
22.174 val SOME (t3',_) = common_nominators_ thy t3;
22.175 val SOME (t3'',_) = add_fractions_ thy t3;
22.176 (term2str t3');
22.177 (term2str t3'');
22.178
22.179 -val t3 = (term_of o the o (parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x - 2)) + ((1) / ( x^^^2 - 1))+((1) / (x^^^2 - 2 * x + 1))";
22.180 +val t3 = (Thm.term_of o the o (parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x - 2)) + ((1) / ( x^^^2 - 1))+((1) / (x^^^2 - 2 * x + 1))";
22.181 val SOME (t3',_) = common_expanded_nom_ thy t3;
22.182 val SOME (t3'',_) = add_expanded_frac_ thy t3;
22.183 (term2str t3');
22.184 @@ -787,10 +787,10 @@
22.185 term2str t4;
22.186 term2str (hd(t5));*)
22.187
22.188 -(*val test1 = (term_of o the o (parse thy)) "1 - x^^^2 - 5 * x^^^5";
22.189 -val test2 = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^ 5";
22.190 -val test2 = (term_of o the o (parse thy)) "1 - x";
22.191 -val test2 = (term_of o the o (parse thy)) "1 + (-1) * x";
22.192 +(*val test1 = (Thm.term_of o the o (parse thy)) "1 - x^^^2 - 5 * x^^^5";
22.193 +val test2 = (Thm.term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^ 5";
22.194 +val test2 = (Thm.term_of o the o (parse thy)) "1 - x";
22.195 +val test2 = (Thm.term_of o the o (parse thy)) "1 + (-1) * x";
22.196 term2str(expanded2term(test1));
22.197 term2str(term2expanded(test2)); *)
22.198
22.199 @@ -798,7 +798,7 @@
22.200
22.201 (* WN kopiert 16.10.02 Rational.ML -> rational.sml-----vvv---*)
22.202
22.203 - val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)";
22.204 + val t=(Thm.term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)";
22.205 val SOME (t',_) = factout_ thy t;
22.206 val SOME (t'',_) = cancel_ thy t;
22.207 term2str t';
22.208 @@ -806,7 +806,7 @@
22.209 "(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
22.210 "(3 + x) / (3 - x)";
22.211
22.212 - val t=(term_of o the o(parse thy))
22.213 + val t=(Thm.term_of o the o(parse thy))
22.214 "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)";
22.215 val SOME (t',_) = common_nominator_ thy t;
22.216 val SOME (t'',_) = add_fraction_ thy t;
22.217 @@ -816,7 +816,7 @@
22.218 "(4 + x) / (3 - x)";
22.219
22.220 (*WN.16.10.02 hinzugef"ugt -----vv---*)
22.221 - val t=(term_of o the o(parse thy))
22.222 + val t=(Thm.term_of o the o(parse thy))
22.223 "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1";
22.224 val SOME (t',_) = common_nominator_ thy t;
22.225 val SOME (t'',_) = add_fraction_ thy t;
22.226 @@ -826,7 +826,7 @@
22.227 \1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
22.228 "6 / (3 - x)";
22.229
22.230 - val t=(term_of o the o(parse thy))
22.231 + val t=(Thm.term_of o the o(parse thy))
22.232 "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)";
22.233 val SOME (t',_) = common_nominator_ thy t;
22.234 val SOME (t'',_) = add_fraction_ thy t;
22.235 @@ -837,7 +837,7 @@
22.236 "6 / (3 - x)";
22.237 (*WN.16.10.02 hinzugef"ugt -----^^---*)
22.238
22.239 - val t=(term_of o the o (parse thy))
22.240 + val t=(Thm.term_of o the o (parse thy))
22.241 "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
22.242 val SOME (t',_) = factout_ thy t;
22.243 val SOME (t'',_) = cancel_ thy t;
22.244 @@ -846,7 +846,7 @@
22.245 "(y + x) * (y - x) / ((y - x) * (y - x))";
22.246 "(y + x) / (y - x)";
22.247
22.248 - val t=(term_of o the o (parse thy))
22.249 + val t=(Thm.term_of o the o (parse thy))
22.250 "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)";
22.251 val SOME (t',_) = common_nominator_ thy t;
22.252 val SOME (t'',_) = add_fraction_ thy t;
22.253 @@ -857,7 +857,7 @@
22.254 "((-1) - x - y) / (x - y)";
22.255 (*WN.16.10.02 ^^^^^^^ Reihenfolge aus Angabe umgekehrt ?!*)
22.256
22.257 - val t=(term_of o the o (parse thy))
22.258 + val t=(Thm.term_of o the o (parse thy))
22.259 "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
22.260 val SOME (t',_) = common_nominator_ thy t;
22.261 val SOME (t'',_) = add_fraction_ thy t;
22.262 @@ -868,7 +868,7 @@
22.263 "((-1) - y - x) / (y - x)";
22.264 (*WN.16.10.02 ^^^^^^^ lexicographische Ordnung ?!*)
22.265
22.266 - val t=(term_of o the o (parse thy))
22.267 + val t=(Thm.term_of o the o (parse thy))
22.268 "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
22.269 val SOME (t',_) = norm_expanded_rat_ thy t;
22.270 term2str t';
22.271 @@ -878,7 +878,7 @@
22.272 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
22.273 WN.16.10.02 ?!*)
22.274
22.275 - val t=(term_of o the o (parse thy))
22.276 + val t=(Thm.term_of o the o (parse thy))
22.277 "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
22.278 val SOME (t',_) = norm_expanded_rat_ thy t;
22.279 term2str t';
22.280 @@ -888,7 +888,7 @@
22.281 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
22.282 WN.16.10.02 ?!*)
22.283
22.284 - val t=(term_of o the o (parse thy))
22.285 + val t=(Thm.term_of o the o (parse thy))
22.286 "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)";
22.287 val SOME (t',_) = norm_expanded_rat_ thy t;
22.288 val SOME (t'',_) = norm_rational_ thy t;
23.1 --- a/test/Tools/isac/Knowledge/rational.sml Mon Dec 07 11:32:12 2015 +0100
23.2 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Dec 07 14:10:59 2015 +0100
23.3 @@ -91,7 +91,7 @@
23.4 val vs = ["x","y","z"]
23.5 (*precondition for [(c, es),...]: legth es = length vs*)
23.6 ;
23.7 -if term2str (term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5"
23.8 +if term2str (Thm.term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5"
23.9 then () else error "term_of_poly 1 changed";
23.10
23.11 "-------- integration lev.1 fun factout_p_ -----------------------------------";
23.12 @@ -721,8 +721,8 @@
23.13 ### Isabelle2009-2 for cancel_ (not cancel_p_):
23.14 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
23.15 andalso string_of_thm thm =
23.16 - (string_of_thm o make_thm o (cterm_of (@{theory "Isac"})))
23.17 - (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
23.18 + (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac"})))
23.19 + (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
23.20 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
23.21 \---------------------------------------------------------------------------------------/*)
23.22
23.23 @@ -740,8 +740,8 @@
23.24 (* find the next rule to apply *)
23.25 val SOME (r as (Thm (str, thm))) = nex revsets t;
23.26 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
23.27 - string_of_thm thm = (string_of_thm o make_thm o (cterm_of (@{theory "Isac"})))
23.28 - (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
23.29 + string_of_thm thm = (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac"})))
23.30 + (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
23.31 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
23.32
23.33 (*check the next rule*)
23.34 @@ -1604,7 +1604,7 @@
23.35 "-------- fun eval_get_denominator -------------------------------------------";
23.36 "-------- fun eval_get_denominator -------------------------------------------";
23.37 val thy = @{theory Isac};
23.38 -val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
23.39 +val t = Thm.term_of (the (parse thy "get_denominator ((a +x)/b)"));
23.40 val SOME (_, t') = eval_get_denominator "" 0 t thy;
23.41 if term2str t' = "get_denominator ((a + x) / b) = b"
23.42 then () else error "get_denominator ((a + x) / b) = b"
24.1 --- a/test/Tools/isac/Knowledge/rlang.sml Mon Dec 07 11:32:12 2015 +0100
24.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Mon Dec 07 14:10:59 2015 +0100
24.3 @@ -206,9 +206,9 @@
24.4 | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []";
24.5
24.6 (*WN---v *)
24.7 -val bdv= (term_of o the o (parse thy)) "bdv";
24.8 -val v = (term_of o the o (parse thy)) "x";
24.9 -val t = (term_of o the o (parse thy)) "3 * x / 5";
24.10 +val bdv= (Thm.term_of o the o (parse thy)) "bdv";
24.11 +val v = (Thm.term_of o the o (parse thy)) "x";
24.12 +val t = (Thm.term_of o the o (parse thy)) "3 * x / 5";
24.13 val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true
24.14 [(bdv, v)] make_ratpoly_in t;
24.15 if term2str t' = "3 / 5 * x" then () else error "rlang.sml: 1";
25.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Mon Dec 07 11:32:12 2015 +0100
25.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Mon Dec 07 14:10:59 2015 +0100
25.3 @@ -18,62 +18,62 @@
25.4
25.5 (*=== inhibit exn ?=============================================================
25.6
25.7 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
25.8 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
25.9 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.10 val result = term2str t_;
25.11 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
25.12
25.13 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
25.14 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
25.15 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.16 val result = term2str t_;
25.17 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
25.18
25.19 -val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x";
25.20 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x";
25.21 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.22 val result = term2str t_;
25.23 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
25.24
25.25 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x";
25.26 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x";
25.27 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.28 val result = term2str t_;
25.29 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
25.30
25.31 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x";
25.32 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x";
25.33 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.34 val result = term2str t_;
25.35 if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
25.36
25.37 -val t = (term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
25.38 +val t = (Thm.term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
25.39 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.40 val result = term2str t_;
25.41 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
25.42
25.43 -val t = (term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
25.44 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
25.45 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.46 val result = term2str t_;
25.47 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
25.48
25.49 -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
25.50 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
25.51 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.52 val result = term2str t_;
25.53 if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
25.54
25.55 -val t = (term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
25.56 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
25.57 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.58 val result = term2str t_;
25.59 if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
25.60
25.61 -val t = (term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
25.62 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
25.63 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.64 val result = term2str t_;
25.65 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
25.66
25.67 -val t = (term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
25.68 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
25.69 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.70 val result = term2str t_;
25.71 if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else ();
25.72
25.73 -val t = (term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
25.74 +val t = (Thm.term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
25.75 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
25.76 val result = term2str t_;
25.77 if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else ();
26.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Mon Dec 07 11:32:12 2015 +0100
26.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Mon Dec 07 14:10:59 2015 +0100
26.3 @@ -18,37 +18,37 @@
26.4 "------------ tests on predicates -------------------------------";
26.5 "------------ tests on predicates -------------------------------";
26.6 "------------ tests on predicates -------------------------------";
26.7 -val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
26.8 +val t1 = (Thm.term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x";
26.9 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
26.10 if (term2str t) = "False" then ()
26.11 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
26.12
26.13 -val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
26.14 +val t1 = (Thm.term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x";
26.15 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
26.16 if (term2str t) = "False" then ()
26.17 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
26.18
26.19 -val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
26.20 +val t1 = (Thm.term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x";
26.21 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
26.22 if (term2str t) = "False" then ()
26.23 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
26.24
26.25 -val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
26.26 +val t1 = (Thm.term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
26.27 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
26.28 if (term2str t) = "True" then ()
26.29 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
26.30
26.31 -val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
26.32 +val t1 = (Thm.term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
26.33 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
26.34 if (term2str t) = "True" then ()
26.35 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
26.36
26.37 -val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
26.38 +val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
26.39 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
26.40 if (term2str t) = "True" then ()
26.41 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
26.42
26.43 -val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
26.44 +val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
26.45 val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1;
26.46 if (term2str t) = "True" then ()
26.47 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
27.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Dec 07 11:32:12 2015 +0100
27.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Mon Dec 07 14:10:59 2015 +0100
27.3 @@ -30,7 +30,7 @@
27.4
27.5
27.6 (*
27.7 -> val t = (term_of o the o (parse thy)) "#2^^^#3";
27.8 +> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
27.9 > val eval_fn = the (assoc (!eval_list, "pow"));
27.10 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
27.11 > Syntax.string_of_term (thy2ctxt thy) t';
27.12 @@ -120,7 +120,7 @@
27.13 parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
27.14 (* 31.1.00
27.15 val tag__forms = chktyps thy (formals, givens);
27.16 -map ((atomty) o term_of) tag__forms; *)
27.17 +map ((atomty) o Thm.term_of) tag__forms; *)
27.18
27.19 " --- subproblem 2: linear-equation --- ";
27.20 val origin = ["x + 4 = (0::real)","x::real"];
27.21 @@ -135,14 +135,14 @@
27.22 val givens = map (the o (parse thy)) given;
27.23
27.24 val tag__forms = chktyps thy (formals, givens);
27.25 -map ((atomty) o term_of) tag__forms;
27.26 +map ((atomty) o Thm.term_of) tag__forms;
27.27
27.28
27.29
27.30 " _________________ rewrite_ x+4_________________ ";
27.31 " _________________ rewrite_ x+4_________________ ";
27.32 " _________________ rewrite_ x+4_________________ ";
27.33 -val t = (term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
27.34 +val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
27.35 val thm = num_str @{thm square_equation_left};
27.36 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
27.37 val rls = Test_simplify;
27.38 @@ -210,8 +210,8 @@
27.39 " _________________ rewrite x=4_________________ ";
27.40 (*
27.41 rewrite thy' "tless_true" "tval_rls" true (num_str @{thm rbinom_power_2}) ct;
27.42 -atomty ((#prop o rep_thm) (!tthm));
27.43 -atomty (term_of (!tct));
27.44 +atomty ((#prop o Thm.rep_thm) (!tthm));
27.45 +atomty (Thm.term_of (!tct));
27.46 *)
27.47 val thy' = "Test";
27.48 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
27.49 @@ -385,7 +385,7 @@
27.50 *)
27.51
27.52 (*
27.53 -val t = (term_of o the o (parse thy)) "solutions (L::real set)";
27.54 +val t = (Thm.term_of o the o (parse thy)) "solutions (L::real set)";
27.55 atomty t;
27.56 *)
27.57
27.58 @@ -573,7 +573,7 @@
27.59
27.60
27.61
27.62 -val ttt = (term_of o the o (parse Test.thy))
27.63 +val ttt = (Thm.term_of o the o (parse Test.thy))
27.64 "Let (((While contains_root e_e Do\
27.65 \Rewrite square_equation_left True @@\
27.66 \Try (Rewrite_Set Test_simplify False) @@\
28.1 --- a/test/Tools/isac/OLDTESTS/script.sml Mon Dec 07 11:32:12 2015 +0100
28.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Mon Dec 07 14:10:59 2015 +0100
28.3 @@ -74,7 +74,7 @@
28.4 \ [BOOL e_2, REAL v_2])\
28.5 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
28.6
28.7 -val ags = map (term_of o the o (parse DiffApp.thy))
28.8 +val ags = map (Thm.term_of o the o (parse DiffApp.thy))
28.9 ["A::real", "alpha::real",
28.10 "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"];
28.11 val ll = [](*:loc_*);
28.12 @@ -156,7 +156,7 @@
28.13 (*#####################################################--------11.5.02
28.14 "################ Solve_root_equation #################";
28.15 (*#####################################################*)
28.16 -val sc = (term_of o the o (parse Test.thy))
28.17 +val sc = (Thm.term_of o the o (parse Test.thy))
28.18 "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
28.19 \ (let e_e = Rewrite square_equation_left True eq_; \
28.20 \ e_e = Rewrite_Set Test_simplify False e_; \
28.21 @@ -172,7 +172,7 @@
28.22 \ e_e = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\
28.23 \ e_e = Rewrite_Set Test_simplify False e_e \
28.24 \ in [e_::bool])";
28.25 -val ags = map (term_of o the o (parse Test.thy))
28.26 +val ags = map (Thm.term_of o the o (parse Test.thy))
28.27 ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"];
28.28 val fmz =
28.29 ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
28.30 @@ -248,7 +248,7 @@
28.31 " --- test100: nxt_tac order------------------------------------ ";
28.32
28.33 val scr as (Prog sc) = Prog (((inst_abs Test.thy)
28.34 - o term_of o the o (parse thy))
28.35 + o Thm.term_of o the o (parse thy))
28.36 "Script Testeq (e_e::bool) = \
28.37 \(While (contains_root e_e) Do \
28.38 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
28.39 @@ -266,10 +266,10 @@
28.40 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*)
28.41 val (p,_,_,_,_,pt) = me nxt p c pt;
28.42 val p = ([1],Res):pos';
28.43 -val eq_ = (term_of o the o (parse thy))"e_::bool";
28.44 +val eq_ = (Thm.term_of o the o (parse thy))"e_::bool";
28.45
28.46 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0";
28.47 -val ve0_= (term_of o the o (parse thy)) ct;
28.48 +val ve0_= (Thm.term_of o the o (parse thy)) ct;
28.49 val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
28.50 e_term,e_term,Safe)),
28.51 ([],(User', [], [], e_term, e_term,Sundef))]:ets;
28.52 @@ -282,14 +282,14 @@
28.53
28.54
28.55 val scr as (Prog sc) =
28.56 - Prog (((inst_abs Test.thy) o term_of o the o (parse thy))
28.57 + Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy))
28.58 "Script Testterm (g_::real) = (Calculate cancel g_)");
28.59 (*
28.60 val scr as (Prog sc) =
28.61 - Prog (((inst_abs Test.thy) o term_of o the o (parse thy))
28.62 + Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy))
28.63 "Script Testterm (g_::real) = (Calculate power g_)");
28.64 val scr as (Prog sc) =
28.65 - Prog (((inst_abs Test.thy) o term_of o the o (parse thy))
28.66 + Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy))
28.67 "Script Testterm (g_::real) = (Calculate pow g_)");
28.68 ..............................................................*)
28.69 writeln
29.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Mon Dec 07 11:32:12 2015 +0100
29.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Mon Dec 07 14:10:59 2015 +0100
29.3 @@ -9,35 +9,35 @@
29.4 (*---------------- 25.7.02 ---------------------*)
29.5
29.6 val thy = (theory "Isac");
29.7 -val t = (term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";
29.8 +val t = (Thm.term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";
29.9 val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy;
29.10
29.11 -val t = (term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x";
29.12 +val t = (Thm.term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x";
29.13 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
29.14
29.15 (*---
29.16 -val v = (term_of o the o (parse thy)) "x";
29.17 -val t = (term_of o the o (parse thy)) "sqrt(#3+#4*x)";
29.18 +val v = (Thm.term_of o the o (parse thy)) "x";
29.19 +val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*x)";
29.20 scan t v;
29.21 -val t = (term_of o the o (parse thy)) "sqrt(#3+#4*a)";
29.22 +val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*a)";
29.23 scan t v;
29.24 -val t = (term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";
29.25 +val t = (Thm.term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)";
29.26 scan t v;
29.27 -val t = (term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";
29.28 +val t = (Thm.term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)";
29.29 scan t v;
29.30 ---*)
29.31 -val t = (term_of o the o (parse thy))
29.32 +val t = (Thm.term_of o the o (parse thy))
29.33 "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x";
29.34 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
29.35
29.36 -val t = (term_of o the o (parse thy))
29.37 +val t = (Thm.term_of o the o (parse thy))
29.38 "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x";
29.39 val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy;
29.40
29.41 -val t = (term_of o the o (parse Test.thy))
29.42 +val t = (Thm.term_of o the o (parse Test.thy))
29.43 "is_rootequation_in (sqrt(x)=1) x";
29.44 atomty t;
29.45 -val t = (term_of o the o (parse (theory "Isac")))
29.46 +val t = (Thm.term_of o the o (parse (theory "Isac")))
29.47 "is_rootequation_in (sqrt(x)=1) x";
29.48 atomty t;
29.49
30.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Mon Dec 07 11:32:12 2015 +0100
30.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Mon Dec 07 14:10:59 2015 +0100
30.3 @@ -483,7 +483,7 @@
30.4
30.5
30.6 (*GoOn.5.03. script with Map, Subst (biquadr.equ.)
30.7 -val scr = Prog (((inst_abs thy) o term_of o the o (parse thy))
30.8 +val scr = Prog (((inst_abs thy) o Thm.term_of o the o (parse thy))
30.9 "Script Biquadrat_poly (e_e::bool) (v_::real) = \
30.10 \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \
30.11 \ L_0_ = (SubProblem (PolyEq_,[univariate,equation], [no_met]) \
31.1 --- a/test/Tools/isac/ProgLang/calculate.sml Mon Dec 07 11:32:12 2015 +0100
31.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Mon Dec 07 14:10:59 2015 +0100
31.3 @@ -32,7 +32,7 @@
31.4 val cal = snd (assoc_calc' thy "is_polyexp");
31.5 val t = @{term "(x / x) is_polyexp"};
31.6 val SOME (thmID, thm) = get_calculation_ thy cal t;
31.7 -(HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop")
31.8 +(HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
31.9 handle TERM _ =>
31.10 error "calculate.sml: get_calculation_ must return Trueprop";
31.11
31.12 @@ -41,12 +41,12 @@
31.13 "----------- fun calculate_ -----------------------------";
31.14 val thy = @{theory "Test"};
31.15 "===== test 1";
31.16 -val t = (term_of o the o (parse thy)) "1+2";
31.17 +val t = (Thm.term_of o the o (parse thy)) "1+2";
31.18 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
31.19 term2str (prop_of thm) = "1 + 2 = 3";
31.20
31.21 "===== test 2";
31.22 -val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
31.23 +val t = (Thm.term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
31.24 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
31.25 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
31.26 if term2str t = "(3 * 4 / 3) ^^^ 2" then ()
31.27 @@ -131,7 +131,7 @@
31.28
31.29 (*--------------(2): does divide work in Test_simplify ?: ------*)
31.30 val thy = @{theory Test};
31.31 - val t = (term_of o the o (parse thy)) "6 / 2";
31.32 + val t = (Thm.term_of o the o (parse thy)) "6 / 2";
31.33 val rls = Test_simplify;
31.34 val (t,_) = the (rewrite_set_ thy false rls t);
31.35 (*val t = Free ("3","Real.real") : term*)
31.36 @@ -145,7 +145,7 @@
31.37
31.38
31.39 (*--------------(3): is_const works ?: -------------------------------------*)
31.40 - val t = (term_of o the o (parse @{theory Test})) "2 is_const";
31.41 + val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const";
31.42 atomty t;
31.43 rewrite_set_ @{theory Test} false tval_rls t;
31.44 (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
31.45 @@ -161,7 +161,7 @@
31.46 (*-------------- eval_cancel works: *)
31.47 trace_rewrite:=false;
31.48 val thy = @{theory Test};
31.49 - val t = (term_of o the o (parse thy)) "(-4) / 2";
31.50 + val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
31.51
31.52 val SOME (_, t) = eval_cancel "xxx" "Fields.inverse_class.divide" t thy;
31.53
31.54 @@ -282,7 +282,7 @@
31.55 "----------- Atools.pow Power.power_class.power ---------";
31.56 "----------- Atools.pow Power.power_class.power ---------";
31.57 "----------- Atools.pow Power.power_class.power ---------";
31.58 -val t = (term_of o the o (parseold thy)) "1 ^ aaa";
31.59 +val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa";
31.60 atomty t;
31.61 (*** -------------
31.62 *** Const ( Nat.power, ['a, nat] => 'a)
31.63 @@ -302,17 +302,17 @@
31.64 " ================= calculate.sml: calculate_ 2002 =================== ";
31.65
31.66 val thy = @{theory Test};
31.67 -val t = (term_of o the o (parse thy)) "12 / 3";
31.68 +val t = (Thm.term_of o the o (parse thy)) "12 / 3";
31.69 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
31.70 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
31.71 "12 / 3 = 4";
31.72 val thy = @{theory Test};
31.73 -val t = (term_of o the o (parse thy)) "4 ^^^ 2";
31.74 +val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2";
31.75 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t;
31.76 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
31.77 "4 ^ 2 = 16";
31.78
31.79 - val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
31.80 + val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
31.81 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
31.82 "1 + 2 = 3";
31.83 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
31.84 @@ -337,7 +337,7 @@
31.85 else ();
31.86
31.87 (*13.9.02 *** calc: operator = pow not defined*)
31.88 - val t = (term_of o the o (parse thy)) "3^^^2";
31.89 + val t = (Thm.term_of o the o (parse thy)) "3^^^2";
31.90 val SOME (thmID,thm) =
31.91 get_calculation_ thy (the(assoc(calclist,"POWER"))) t;
31.92 (*** calc: operator = pow not defined*)
32.1 --- a/test/Tools/isac/ProgLang/listC.sml Mon Dec 07 11:32:12 2015 +0100
32.2 +++ b/test/Tools/isac/ProgLang/listC.sml Mon Dec 07 14:10:59 2015 +0100
32.3 @@ -21,7 +21,7 @@
32.4
32.5 val t = str2term "NTH 1 [a,b,c,d,e]";
32.6 atomty t;
32.7 -val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL};
32.8 +val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_NIL};
32.9 atomty thm;
32.10 val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_NIL}) t;
32.11 if term2str t' = "a" then ()
32.12 @@ -32,7 +32,7 @@
32.13 (Const ("List.list.Cons", _) $ Free ("b", _) $
32.14 (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t;
32.15 atomty t;
32.16 -val thm = (#prop o rep_thm o num_str) @{thm NTH_CONS};
32.17 +val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_CONS};
32.18 atomty thm;
32.19 val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_CONS}) t;
32.20 if term2str t' = "NTH (3 + -1) [b, c, d, e]" then ()
33.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Dec 07 11:32:12 2015 +0100
33.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Mon Dec 07 14:10:59 2015 +0100
33.3 @@ -36,10 +36,10 @@
33.4 val thy = @{theory Complex_Main};
33.5 val ctxt = @{context};
33.6 val thm = @{thm add.commute};
33.7 -val t = (term_of o the) (parse thy "((r + u) + t) + s");
33.8 +val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
33.9 "----- from old: fun rewrite__";
33.10 val bdv = [];
33.11 -val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
33.12 +val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm);
33.13 "----- from old: and rew_sub";
33.14 val (LHS,RHS) = (dest_equals' o strip_trueprop
33.15 o Logic.strip_imp_concl) r;
33.16 @@ -162,11 +162,11 @@
33.17 "----------- step through 'and rew_sub': ----------------";
33.18 (*and make asms without Trueprop, beginning with the result:*)
33.19 val tm = @{term "x*y / y::real"};
33.20 -val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
33.21 +val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (Thm.prop_of thm) tm;
33.22 (*show_types := false;*)
33.23 "----- evaluate arguments";
33.24 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
33.25 - (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
33.26 + (thy, 0, [], dummy_ord, e_rls, true, [], (Thm.prop_of thm), tm);
33.27 "----- step 1: LHS, RHS of rule";
33.28 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
33.29 o Logic.strip_imp_concl) r;
33.30 @@ -315,7 +315,7 @@
33.31 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
33.32 (*t' = t''; (*false because of further rewrites in t'*)*)
33.33 "----- rew_sub --------------------------------";
33.34 -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
33.35 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
33.36 (*t'' = t'''; (*true*)*)
33.37 "----- rewrite_set_ erls --------------------------------";
33.38 val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
33.39 @@ -334,7 +334,7 @@
33.40 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
33.41 (*t' = t''; (*false because of further rewrites in t'*)*)
33.42 writeln "----- rew_sub --------------------------------";
33.43 -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
33.44 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
33.45 (*t'' = t'''; (*true*)*)
33.46 writeln "----- rewrite_set_ erls --------------------------------";
33.47 val cond = @{term "(x / x ^^^ 2)"};
33.48 @@ -502,7 +502,7 @@
33.49 "----------- 2011 thms with axclasses -------------------";
33.50 "----------- 2011 thms with axclasses -------------------";
33.51 val thm = num_str @{thm divide_1};
33.52 -val prop = prop_of thm;
33.53 +val prop = Thm.prop_of thm;
33.54 atomty prop; (*Type 'a*)
33.55 val t = str2term "(2*x)/1"; (*Type real*)
33.56
34.1 --- a/test/Tools/isac/ProgLang/termC.sml Mon Dec 07 11:32:12 2015 +0100
34.2 +++ b/test/Tools/isac/ProgLang/termC.sml Mon Dec 07 14:10:59 2015 +0100
34.3 @@ -169,17 +169,17 @@
34.4 "----------- inst_bdv -----------------------------------";
34.5 "----------- inst_bdv -----------------------------------";
34.6 "----------- inst_bdv -----------------------------------";
34.7 - if (term2str o prop_of o num_str) @{thm d1_isolate_add2} =
34.8 + if (term2str o Thm.prop_of o num_str) @{thm d1_isolate_add2} =
34.9 "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)"
34.10 then ()
34.11 else error "termC.sml d1_isolate_add2";
34.12 val subst = [(str2term "bdv", str2term "x")];
34.13 - val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
34.14 + val t = (norm o #prop o Thm.rep_thm) (num_str @{thm d1_isolate_add2});
34.15 val t' = inst_bdv subst t;
34.16 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)"
34.17 then ()
34.18 else error "termC.sml inst_bdv 1";
34.19 -if (term2str o prop_of o num_str) @{thm separate_bdvs_add} =
34.20 +if (term2str o Thm.prop_of o num_str) @{thm separate_bdvs_add} =
34.21 "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n==>" ^
34.22 " (?a + ?b = ?c) = (?b = ?c + -1 * ?a)"
34.23 then () else error "termC.sml separate_bdvs_add";
34.24 @@ -190,7 +190,7 @@
34.25 (str2term "bdv_2", str2term "c_2"),
34.26 (str2term "bdv_3", str2term "c_3"),
34.27 (str2term "bdv_4", str2term "c_4")];
34.28 -val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
34.29 +val t = (norm o #prop o Thm.rep_thm) (num_str @{thm separate_bdvs_add});
34.30 val t' = inst_bdv subst t;
34.31
34.32 if term2str t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
34.33 @@ -218,8 +218,8 @@
34.34 "----------- Pattern.match ------------------------------";
34.35 "----------- Pattern.match ------------------------------";
34.36 "----------- Pattern.match ------------------------------";
34.37 - val t = (term_of o the o (parse thy)) "3 * x^^^2 = (1::real)";
34.38 - val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)";
34.39 + val t = (Thm.term_of o the o (parse thy)) "3 * x^^^2 = (1::real)";
34.40 + val pat = (free2var o Thm.term_of o the o (parse thy)) "a * b^^^2 = (c::real)";
34.41 (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*)
34.42 val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty);
34.43 default_print_depth 3; (*999*) insts;
34.44 @@ -329,7 +329,7 @@
34.45 val t = (Syntax.read_term_global thy str);
34.46 val t = numbers_to_string (Syntax.read_term_global thy str);
34.47 val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
34.48 - cterm_of thy t;
34.49 + Thm.global_cterm_of thy t;
34.50 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
34.51
34.52 "===== fun parse_patt caused error in fun T_a2real ===";
34.53 @@ -344,7 +344,7 @@
34.54 val t = (Syntax.read_term_global thy str);
34.55 val t = numbers_to_string (Syntax.read_term_global thy str);
34.56 val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
34.57 - cterm_of thy t;
34.58 + Thm.global_cterm_of thy t;
34.59 val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed";
34.60
34.61 "===== fun parse_patt caused error in fun T_a2real ===";
35.1 --- a/test/Tools/isac/calcelems.sml Mon Dec 07 11:32:12 2015 +0100
35.2 +++ b/test/Tools/isac/calcelems.sml Mon Dec 07 14:10:59 2015 +0100
35.3 @@ -81,7 +81,7 @@
35.4 fun parse thy str =
35.5 (let val t = (typ_a2real o numbers_to_string)
35.6 (Syntax.read_term_global thy str)
35.7 - in SOME (cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
35.8 + in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*)
35.9 handle _ => NONE;
35.10 *)
35.11
36.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Dec 07 11:32:12 2015 +0100
36.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Dec 07 14:10:59 2015 +0100
36.3 @@ -17,7 +17,7 @@
36.4 "----------- ### thes2file ... Exception- Match raised -----------";
36.5 "----------- search for data error in thes2file ------------------";
36.6 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
36.7 -"----------- fun make_thm ----------------------------------------";
36.8 +"----------- fun Thm.make_thm ------------------------------------";
36.9 "----------- correct theIDs for e_rls ----------------------------";
36.10 "----------- correct theIDs for list_rls -------------------------";
36.11 "----------- fun revert_sym --------------------------------------";
36.12 @@ -121,12 +121,12 @@
36.13 ;
36.14 thydata2xml (theID, thydata);
36.15
36.16 -"----------- fun make_thm ----------------------------------------";
36.17 -"----------- fun make_thm ----------------------------------------";
36.18 -"----------- fun make_thm ----------------------------------------";
36.19 -"~~~~~ fun make_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) =
36.20 +"----------- fun Thm.make_thm ------------------------------------";
36.21 +"----------- fun Thm.make_thm ------------------------------------";
36.22 +"----------- fun Thm.make_thm ------------------------------------";
36.23 +"~~~~~ fun Thm.make_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) =
36.24 (@{theory "Biegelinie"}, "IsacKnowledge",
36.25 - ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft}),
36.26 + ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
36.27 ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
36.28 val guh = thm2guh (part, theory2thyID thy) thmID
36.29 val theID = guh2theID guh;
36.30 @@ -196,7 +196,7 @@
36.31 |> map (revert_sym thy)
36.32 (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
36.33 Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
36.34 - |> map (fn Thm (thmID, thm) => (thmID, prop_of thm))
36.35 + |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))
36.36 (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,
36.37 ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)
36.38 |> gen_distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);