# HG changeset patch # User Walther Neuper # Date 1449493859 -3600 # Node ID c477d0f79ab903c337afdb70048aa2d1a7da0ebd # Parent 2b26acbd130ccfc1fc9a25ac7b63714935e08c20 Isabelle2014-->15: closed Thm.thy applied to tests Note: # concerns the funs: assbl_thm, cterm_of-->global_cterm_of, make_thm, prop_of, rep_thm, rep_thm_G, therm_of. # tests have not been run since start of Isabelle2014-->15. diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Mon Dec 07 14:10:59 2015 +0100 @@ -35,7 +35,7 @@ text{*Apply the Method to an expression.*} ML{* - val input = term_of (the (parse thy "get_denominator ((a + b) / c)")); + val input = Thm.term_of (the (parse thy "get_denominator ((a + b) / c)")); val SOME (_, output) = eval_get_denominator "" 0 input thy; *} diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Dec 07 14:10:59 2015 +0100 @@ -1076,7 +1076,7 @@ " in X)"; parse thy str; - val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; + val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; atomty sc; *} diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Dec 07 14:10:59 2015 +0100 @@ -88,7 +88,7 @@ will disappear), which does not encode numerals as binary numbers: *} ML {* val SOME t = parse @{theory "Isac"} "a + b * 3"; - atomwy (term_of t); + atomwy (Thm.term_of t); *} text {* From the above we see: the internal representation of a term contains all the knowledge it is built from, see diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Mon Dec 07 14:10:59 2015 +0100 @@ -39,7 +39,7 @@ *} text {* ... and let us differentiate the term t: *} ML {* -val t = (term_of o the o (parse thy)) "d_d x (x^^^2 + x + y)"; +val t = (Thm.term_of o the o (parse thy)) "d_d x (x^^^2 + x + y)"; val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t; val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t; @@ -78,10 +78,10 @@ text {* We have already seen conditional rewriting above when we used the rule diff_const; let us try: *} ML {* -val t1 = (term_of o the o (parse thy)) "d_d x (a*BC*x*z)"; +val t1 = (Thm.term_of o the o (parse thy)) "d_d x (a*BC*x*z)"; rewrite_inst_ thy ro er true inst diff_const t1; -val t2 = (term_of o the o (parse thy)) "d_d x (a*BC*y*z)"; +val t2 = (Thm.term_of o the o (parse thy)) "d_d x (a*BC*y*z)"; rewrite_inst_ thy ro er true inst diff_const t2; *} text {* For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false, @@ -96,7 +96,7 @@ *} ML {* (*show_brackets := true; TODO*) -val t0 = (term_of o the o (parse thy)) "2*a + 3*b + 4*a"; term2str t0; +val t0 = (Thm.term_of o the o (parse thy)) "2*a + 3*b + 4*a"; term2str t0; (*show_brackets := false;*) *} text {* Now we want to bring 4*a close to 2*a in order to get 6*a: @@ -145,11 +145,11 @@ *} ML {* (*show_brackets := false; TODO*) -val t1 = (term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)"; +val t1 = (Thm.term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)"; val SOME (t, _) = rewrite_set_ thy true make_polynomial t1; term2str t; *} ML {* -val t2 = (term_of o the o (parse thy)) +val t2 = (Thm.term_of o the o (parse thy)) "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))"; val SOME (t, _) = rewrite_set_ thy true norm_Rational t2; term2str t; *} @@ -185,7 +185,7 @@ subsection {* What already works *} ML {* -val t2 = (term_of o the o (parse thy)) +val t2 = (Thm.term_of o the o (parse thy)) "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; val SOME (t, _) = rewrite_set_ thy true rls_p_33 t2; term2str t; *} @@ -225,7 +225,7 @@ subsection {* This does not yet work *} ML {* -val t = (term_of o the o (parse thy)) +val t = (Thm.term_of o the o (parse thy)) "(2*a - 5*b) * (2*a + 5*b)"; rewrite_set_ thy true rls_p_33 t; term2str t; *} diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Interpret/calchead.sml --- a/test/Tools/isac/Interpret/calchead.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Dec 07 14:10:59 2015 +0100 @@ -406,10 +406,10 @@ ============ inhibit exn AK110726 ==============================================*) "--------------------------------step through code mtc---"; val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); -cterm_of; +Thm.global_cterm_of; val ttt = (dsc $ var); (*============ inhibit exn AK110726 ============================================== -cterm_of thy (dsc $ var); +Thm.global_cterm_of thy (dsc $ var); ============ inhibit exn AK110726 ==============================================*) "-------------------------------------step through end---"; @@ -497,10 +497,10 @@ -------------------------------------------------------------------*) "--------------------------------step through code mtc---"; val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); -cterm_of; +Thm.global_cterm_of; val ttt = (dsc $ var); (*============ inhibit exn AK110726 ============================================== -cterm_of thy (dsc $ var); +Thm.global_cterm_of thy (dsc $ var); -------------------------------------------------------------------*) "-------------------------------------step through end---"; @@ -554,7 +554,7 @@ "--------------------------------step through code mtc---"; val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); val ttt = (dsc $ var); -cterm_of thy (dsc $ var); +Thm.global_cterm_of thy (dsc $ var); val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori); "-d2-----------------------------------------------------"; @@ -567,7 +567,7 @@ "--------------------------------step through code mtc---"; val (thy, (str, (dsc, _)):pat, ty $ var) = (thy, p, a); val ttt = (dsc $ var); -cterm_of thy (dsc $ var); +Thm.global_cterm_of thy (dsc $ var); val ori = ((([1], str, dsc, (*[var]*) split_dts' (dsc, var))): preori); "-d3-----------------------------------------------------"; pbt = []; (*true, base case*) diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Interpret/inform.sml --- a/test/Tools/isac/Interpret/inform.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Interpret/inform.sml Mon Dec 07 14:10:59 2015 +0100 @@ -1018,7 +1018,7 @@ "~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) = (cs', (encode ifo)); val SOME f_in = parse (assoc_thy "Isac") istr -val f_in = term_of f_in +val f_in = Thm.term_of f_in val pos_pred = lev_back' pos (* f_pred ---"step pos cs"---> f_succ in appendFormula TODO.WN120517: one starting point for redesign of pos' *) diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Interpret/mathengine.sml --- a/test/Tools/isac/Interpret/mathengine.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Interpret/mathengine.sml Mon Dec 07 14:10:59 2015 +0100 @@ -719,7 +719,7 @@ "~~~~~ fun inform, args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) = (cs', (encode ifo)); val SOME f_in = parse (assoc_thy "Isac") istr - val f_in = term_of f_in + val f_in = Thm.term_of f_in val f_succ = get_curr_formula (pt, pos); f_succ = f_in = false; val NONE = cas_input f_in diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Interpret/ptyps.sml --- a/test/Tools/isac/Interpret/ptyps.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Interpret/ptyps.sml Mon Dec 07 14:10:59 2015 +0100 @@ -26,20 +26,20 @@ val ctxt = Proof_Context.init_global @{theory "Isac"}; (*case 1: no refinement *) -val (d1,ts1) = split_dts ((term_of o the o (parse thy)) "fixedValues [aaa = 0]"); -val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "errorBound (ddd = 0)"); +val (d1,ts1) = split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]"); +val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "errorBound (ddd = 0)"); val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: ori list; (*case 2: refined to pbt without children *) -val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "relations [aaa333]"); +val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "relations [aaa333]"); val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list; (*case 3: refined to pbt with children *) -val (d2,ts2) = split_dts ((term_of o the o (parse thy)) "valuesFor [aaa222]"); +val (d2,ts2) = split_dts ((Thm.term_of o the o (parse thy)) "valuesFor [aaa222]"); val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:ori list; (*case 4: refined to children (without child)*) -val (d3,ts3) = split_dts ((term_of o the o (parse thy)) "boundVariable aaa222yyy"); +val (d3,ts3) = split_dts ((Thm.term_of o the o (parse thy)) "boundVariable aaa222yyy"); val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:ori list; (*================================================================= diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Interpret/script.sml --- a/test/Tools/isac/Interpret/script.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Interpret/script.sml Mon Dec 07 14:10:59 2015 +0100 @@ -33,7 +33,7 @@ " (M1__M1::bool) = ((Substitute [v_v = 0])) q___q " ^ " in True)"; -val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str; +val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; val str = (*#2#*) "Script BiegelinieScript " ^ @@ -74,7 +74,7 @@ " in True)" ; -val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str; +val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; atomty sc'; val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; @@ -98,7 +98,7 @@ " M1__M1 = Substitute [e1__e1] M1__M1 " ^ " in True)" ; -val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str; +val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; atomty sc'; val str = (*Substitute @@ Substitute does NOT work???*) diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Mon Dec 07 14:10:59 2015 +0100 @@ -47,7 +47,7 @@ " n_eq = drop_questionmarks n_eq "^(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) "in n_eq)" (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) ; -val sc = ((inst_abs thy) o term_of o the o (parse @{theory Isac})) str; +val sc = ((inst_abs thy) o Thm.term_of o the o (parse @{theory Isac})) str; writeln (term2str sc); "----------- test [SignalProcessing,Z_Transform,inverse_sub] me = "; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/algein.sml --- a/test/Tools/isac/Knowledge/algein.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/algein.sml Mon Dec 07 14:10:59 2015 +0100 @@ -29,7 +29,7 @@ \ (let t_t = (l_l = 1)\ \ in t_t)" ; -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; atomty sc; atomt sc; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/atools.sml --- a/test/Tools/isac/Knowledge/atools.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/atools.sml Mon Dec 07 14:10:59 2015 +0100 @@ -28,7 +28,7 @@ "----------- occurs_in -------------------------------------------"; "----------- occurs_in -------------------------------------------"; (*=========================================================================*) -fun str2t str = (term_of o the o (parse thy)) str; +fun str2t str = (Thm.term_of o the o (parse thy)) str; fun term2s t = term_to_string''' thy t; (*=========================================================================*) @@ -139,14 +139,14 @@ "----------- Matthias Goldgruber 2003 rewrite orders ----"; "----------- Matthias Goldgruber 2003 rewrite orders ----"; (* MK die ersten Tests *) - val substa = [(e_term, (term_of o the o (parse thy)) "a")]; - val substb = [(e_term, (term_of o the o (parse thy)) "b")]; - val substx = [(e_term, (term_of o the o (parse thy)) "x")]; + val substa = [(e_term, (Thm.term_of o the o (parse thy)) "a")]; + val substb = [(e_term, (Thm.term_of o the o (parse thy)) "b")]; + val substx = [(e_term, (Thm.term_of o the o (parse thy)) "x")]; - val x1 = (term_of o the o (parse thy)) "a + b + x"; - val x2 = (term_of o the o (parse thy)) "a + x + b"; - val x3 = (term_of o the o (parse thy)) "a + x + b"; - val x4 = (term_of o the o (parse thy)) "x + a + b"; + val x1 = (Thm.term_of o the o (parse thy)) "a + b + x"; + val x2 = (Thm.term_of o the o (parse thy)) "a + x + b"; + val x3 = (Thm.term_of o the o (parse thy)) "a + x + b"; + val x4 = (Thm.term_of o the o (parse thy)) "x + a + b"; if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then () else error "termorder.sml diff.behav ord_make_polynomial_in #1"; @@ -157,22 +157,22 @@ if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then () else error "termorder.sml diff.behav ord_make_polynomial_in #3"; - val aa = (term_of o the o (parse thy)) "-1 * a * x"; - val bb = (term_of o the o (parse thy)) "x^^^3"; + val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x"; + val bb = (Thm.term_of o the o (parse thy)) "x^^^3"; ord_make_polynomial_in true thy substx (aa, bb); true; (* => LESS *) - val aa = (term_of o the o (parse thy)) "-1 * a * x"; - val bb = (term_of o the o (parse thy)) "x^^^3"; + val aa = (Thm.term_of o the o (parse thy)) "-1 * a * x"; + val bb = (Thm.term_of o the o (parse thy)) "x^^^3"; ord_make_polynomial_in true thy substa (aa, bb); false; (* => GREATER *) (* und nach dem Re-engineering der Termorders in den 'rulesets' kannst Du die 'gr"osste' Variable frei w"ahlen: *) - val bdv= (term_of o the o (parse thy)) "bdv"; - val x = (term_of o the o (parse thy)) "x"; - val a = (term_of o the o (parse thy)) "a"; - val b = (term_of o the o (parse thy)) "b"; + val bdv= (Thm.term_of o the o (parse thy)) "bdv"; + val x = (Thm.term_of o the o (parse thy)) "x"; + val a = (Thm.term_of o the o (parse thy)) "a"; + val b = (Thm.term_of o the o (parse thy)) "b"; val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; if term2str t' = "b + x + a" then () else error "termorder.sml diff.behav ord_make_polynomial_in #11"; @@ -184,7 +184,7 @@ else error "termorder.sml diff.behav ord_make_polynomial_in #13"; val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2"; - val ppp = (term_of o the o (parse thy)) ppp'; + val ppp = (Thm.term_of o the o (parse thy)) ppp'; val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () else error "termorder.sml diff.behav ord_make_polynomial_in #14"; @@ -194,7 +194,7 @@ else error "termorder.sml diff.behav ord_make_polynomial_in #15"; val ttt' = "(3*x + 5)/18"; - val ttt = (term_of o the o (parse thy)) ttt'; + val ttt = (Thm.term_of o the o (parse thy)) ttt'; val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; if term2str uuu = "(5 + 3 * x) / 18" then () else error "termorder.sml diff.behav ord_make_polynomial_in #16a"; @@ -213,7 +213,7 @@ -----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy (*Aufgabe zum Einstieg in die Arbeit...*) - val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0"; + val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0"; (*ein 'ruleset' aus Poly.ML wird angewandt...*) val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t; term2str t; @@ -243,9 +243,9 @@ *) "------15.11.02 --------------------------"; - val t = (term_of o the o (parse thy)) "1 + a * x + b * x"; - val bdv = (term_of o the o (parse thy)) "bdv"; - val a = (term_of o the o (parse thy)) "a"; + val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x"; + val bdv = (Thm.term_of o the o (parse thy)) "bdv"; + val a = (Thm.term_of o the o (parse thy)) "a"; trace_rewrite := false; (* Anwenden einer Regelmenge aus Termorder.ML: *) @@ -257,7 +257,7 @@ term2str t; "1 + b * x + x * a"; - val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2"; + val t = (Thm.term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2"; val SOME (t,_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; term2str t; @@ -266,7 +266,7 @@ term2str t; "1 + (x + b * x) * a + a ^^^ 2"; - val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2"; + val t = (Thm.term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2"; val SOME (t,_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; term2str t; @@ -286,7 +286,7 @@ get_thm Termorder.thy "bdv_n_collect"; get_thm (theory "Isac") "bdv_n_collect"; *) - val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2"; + val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2"; val SOME (t,_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; term2str t; @@ -295,16 +295,16 @@ term2str t; "(7 + x) * a ^^^ 2"; - val t = (term_of o the o (parse Termorder.thy)) "Pi"; + val t = (Thm.term_of o the o (parse Termorder.thy)) "Pi"; - val t = (term_of o the o (parseold thy)) "7"; + val t = (Thm.term_of o the o (parseold thy)) "7"; ##################################################################################*) "----------- fun eval_binop -----------------------------"; "----------- fun eval_binop -----------------------------"; "----------- fun eval_binop -----------------------------"; val (op_, ef) = the (assoc (calclist, "TIMES")); -val t = (term_of o the o (parse thy)) "2 * 3"; +val t = (Thm.term_of o the o (parse thy)) "2 * 3"; (*val SOME (thmid,t') = *)get_pair thy op_ ef t; ; "~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) = diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/biegelinie.sml --- a/test/Tools/isac/Knowledge/biegelinie.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Mon Dec 07 14:10:59 2015 +0100 @@ -22,7 +22,7 @@ val thy = @{theory "Biegelinie"}; val ctxt = thy2ctxt' "Biegelinie"; -fun str2term str = (term_of o the o (parse thy)) str; +fun str2term str = (Thm.term_of o the o (parse thy)) str; fun term2s t = term_to_string'' "Biegelinie" t; fun rewrit thm str = fst (the (rewrite_ thy tless_true e_rls true thm str)); diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/diff.sml Mon Dec 07 14:10:59 2015 +0100 @@ -301,7 +301,7 @@ \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \ \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')" ; -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; "----------- diff_conv, sym_diff_conv -------------------"; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/eqsystem.sml --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon Dec 07 14:10:59 2015 +0100 @@ -93,9 +93,9 @@ else error "eqsystem.sml: length_ [x+y=1,y=2] = 2"; val SOME t = parse thy "solution LL"; -atomty (term_of t); +atomty (Thm.term_of t); val SOME t = parse thy "solution LL"; -atomty (term_of t); +atomty (Thm.term_of t); val t = str2term "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"; @@ -449,7 +449,7 @@ *) > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi; val equalities_es_ = "equalities es_" : string -> val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_; +> val (dd, ii) = (split_did o Thm.term_of o the o (parse thy)) equalities_es_; > show_types:=true; term2str ii; show_types:=false; val it = "es_::bool list" : string ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/inssort.sml --- a/test/Tools/isac/Knowledge/inssort.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/inssort.sml Mon Dec 07 14:10:59 2015 +0100 @@ -117,11 +117,11 @@ (* ------- 17.6.00: mit kleinen problemen aufgegeben -val scr=Prog ((term_of o the o (parse thy)) +val scr=Prog ((Thm.term_of o the o (parse thy)) "Script Sort (u_::'a list) = \ \ Rewrite_Set ins_sort False u_"); -val scr=Prog ((term_of o the o (parse thy)) +val scr=Prog ((Thm.term_of o the o (parse thy)) "Script Ins_sort (u_::real list) = \ \ (let u_ = Rewrite sort_def False u_; \ \ u_ = Rewrite foldr_rec False u_; \ @@ -155,7 +155,7 @@ \ u_ = u_ \ \ in u_)"; -atomty (term_of (the scr)); +atomty (Thm.term_of (the scr)); ------- *) ============ inhibit exn =====================================================*) diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/integrate.sml --- a/test/Tools/isac/Knowledge/integrate.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon Dec 07 14:10:59 2015 +0100 @@ -327,9 +327,9 @@ With =[], Relate=[]}:string ppc; val chkmodel = ((map (the o (parse thy))) o ppc2list) model; -val t1 = (term_of o hd) chkmodel; -val t2 = (term_of o hd o tl) chkmodel; -val t3 = (term_of o hd o tl o tl) chkmodel; +val t1 = (Thm.term_of o hd) chkmodel; +val t2 = (Thm.term_of o hd o tl) chkmodel; +val t3 = (Thm.term_of o hd o tl o tl) chkmodel; case t3 of Const ("Integrate.antiDerivative", _) $ _ => () | _ => error "integrate.sml: Integrate.antiDerivative ???"; @@ -339,9 +339,9 @@ With =[], Relate=[]}:string ppc; val chkmodel = ((map (the o (parse thy))) o ppc2list) model; -val t1 = (term_of o hd) chkmodel; -val t2 = (term_of o hd o tl) chkmodel; -val t3 = (term_of o hd o tl o tl) chkmodel; +val t1 = (Thm.term_of o hd) chkmodel; +val t2 = (Thm.term_of o hd o tl) chkmodel; +val t3 = (Thm.term_of o hd o tl o tl) chkmodel; case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => () | _ => error "integrate.sml: Integrate.antiDerivativeName"; @@ -372,14 +372,14 @@ "Script IntegrationScript (f_f::real) (v_v::real) = \ \ (let t_t = Take (Integral f_f D v_v) \ \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"; -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; atomty sc; val str = "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \ \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \ \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_t)"; -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; atomty sc; show_mets(); diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/poly.sml --- a/test/Tools/isac/Knowledge/poly.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/poly.sml Mon Dec 07 14:10:59 2015 +0100 @@ -38,7 +38,7 @@ "-------- investigate (new 2002) uniary minus -----------"; "-------- investigate (new 2002) uniary minus -----------"; (*---------------------------------------------- vvvvvvvvvvvvvv -----------------------*) -val t = (#prop o rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*) +val t = (#prop o Thm.rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*) atomty t; (* *** Const (HOL.Trueprop, bool => prop) @@ -58,7 +58,7 @@ | _ => error "internal representation of \"0 - ?x = - ?x\" changed"; (*----------------------------------- vvvv --------------------------------------------*) -val t = (term_of o the o (parse thy)) "-1"; +val t = (Thm.term_of o the o (parse thy)) "-1"; atomty t; (*** ------------- *** Free ( -1, real) *) @@ -66,7 +66,7 @@ Free ("-1", _) => () | _ => error "internal representation of \"-1\" changed"; (*----------------------------------- vvvvv -------------------------------------------*) -val t = (term_of o the o (parse thy)) "- 1"; +val t = (Thm.term_of o the o (parse thy)) "- 1"; atomty t; (* *** @@ -80,7 +80,7 @@ "======= these external values all have the same internal representation"; (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*) (*----------------------------------- vvvvv -------------------------------------------*) -val t = (term_of o the o (parse thy)) "-x"; +val t = (Thm.term_of o the o (parse thy)) "-x"; atomty t; (**** ------------- *** Free ( -x, real)*) @@ -88,7 +88,7 @@ Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => () | _ => error "internal representation of \"-x\" changed"; (*----------------------------------- vvvvv -------------------------------------------*) -val t = (term_of o the o (parse thy)) "- x"; +val t = (Thm.term_of o the o (parse thy)) "- x"; atomty t; (**** ------------- *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*) @@ -96,7 +96,7 @@ Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => () | _ => error "internal representation of \"- x\" changed"; (*----------------------------------- vvvvvv ------------------------------------------*) -val t = (term_of o the o (parse thy)) "-(x)"; +val t = (Thm.term_of o the o (parse thy)) "-(x)"; atomty t; (**** ------------- *** Free ( -x, real)*) @@ -338,7 +338,7 @@ if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then () else error "poly.sml: diff.behav. in make_polynomial 23"; "-----SPO ---"; -val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2"; +val t = (Thm.term_of o the o (parse thy)) "a^^^2 * (-a)^^^2"; val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; if (term2str t) = "a ^^^ 4" then () else error "poly.sml: diff.behav. in make_polynomial 24"; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/polyeq.sml --- a/test/Tools/isac/Knowledge/polyeq.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/polyeq.sml Mon Dec 07 14:10:59 2015 +0100 @@ -35,54 +35,54 @@ trace_rewrite:=true; trace_rewrite:=false; *) - val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)"; + val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1; if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then () else error "polyeq.sml: diff.behav. in lhs"; - val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x"; + val t2 = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2; if (term2str t) = "True" then () else error "polyeq.sml: diff.behav. 1 in is_expended_in"; - val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x"; + val t0 = (Thm.term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0; if (term2str t) = "False" then () else error "polyeq.sml: diff.behav. 2 in is_poly_in"; - val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x"; + val t3 = (Thm.term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; if (term2str t) = "True" then () else error "polyeq.sml: diff.behav. 3 in is_poly_in"; - val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x"; + val t4 = (Thm.term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; if (term2str t) = "True" then () else error "polyeq.sml: diff.behav. 4 in is_expended_in"; - val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x"; + val t6 = (Thm.term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6; if (term2str t) = "True" then () else error "polyeq.sml: diff.behav. 5 in is_expended_in"; - val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2"; + val t3 = (Thm.term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; if (term2str t) = "True" then () else error "polyeq.sml: diff.behav. in has_degree_in_in"; - val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2"; + val t3 = (Thm.term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; if (term2str t) = "False" then () else error "polyeq.sml: diff.behav. 6 in has_degree_in_in"; - val t4 = (term_of o the o (parse thy)) + val t4 = (Thm.term_of o the o (parse thy)) "((-8 - 2*x + x^^^2) has_degree_in x) = 1"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; if (term2str t) = "False" then () else error "polyeq.sml: diff.behav. 7 in has_degree_in_in"; - val t5 = (term_of o the o (parse thy)) + val t5 = (Thm.term_of o the o (parse thy)) "((-8 - 2*x + x^^^2) has_degree_in x) = 2"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5; if (term2str t) = "True" then () @@ -833,7 +833,7 @@ "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------"; "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------"; "---- test the erls ----"; - val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1"; + val t1 = (Thm.term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1"; val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1; val t' = term2str t; (*if t'= "HOL.True" then () @@ -1146,14 +1146,14 @@ (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(bdv,x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*) t |> term2str; t |> atomty; val thm = num_str @{thm d2_prescind1}; -thm |> prop_of |> term2str; thm|> prop_of |> atomty; +thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty; val SOME (t', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t; term2str t'; (*x * (-6 + 5 * x) = 0 : Rewrite_Inst (["(bdv,x)"],("d2_reduce_equation1","")) --> x = 0 | -6 + 5 * x = 0*) t' |> term2str; t' |> atomty; val thm = num_str @{thm d2_reduce_equation1}; -thm |> prop_of |> term2str; thm|> prop_of |> atomty; +thm |> Thm.prop_of |> term2str; thm |> Thm.prop_of |> atomty; val SOME (t'', _) = rewrite_inst_ thy e_rew_ord e_rls true subst thm t'; term2str t''; (* NONE with d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" instead d2_reduce_equation1: "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/polyminus.sml --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Dec 07 14:10:59 2015 +0100 @@ -238,7 +238,7 @@ \ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \ \ (Try (Rewrite_Set fasse_zusammen False)) @@ \ \ (Try (Rewrite_Set verschoenere False))) t_t)" -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; atomty sc; "----------- me simplification.for_polynomials.with_minus"; @@ -344,7 +344,7 @@ \ in (Repeat((Try (Repeat (Calculate TIMES))) @@ \ \ (Try (Repeat (Calculate PLUS ))) @@ \ \ (Try (Repeat (Calculate MINUS))))) e_e)" -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; +val sc = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str; atomty sc; "----------- pbl polynom probe -----------------------------------"; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/rateq.sml --- a/test/Tools/isac/Knowledge/rateq.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/rateq.sml Mon Dec 07 14:10:59 2015 +0100 @@ -19,22 +19,22 @@ "------------ pbl: rational, univariate, equation ----------------"; "------------ pbl: rational, univariate, equation ----------------"; "------------ pbl: rational, univariate, equation ----------------"; -val t = (term_of o the o (parse thy)) "(1/b+1/x=1) is_ratequation_in x"; +val t = (Thm.term_of o the o (parse thy)) "(1/b+1/x=1) is_ratequation_in x"; val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t; val result = term2str t_; if result <> "True" then error "rateq.sml: new behaviour 1:" else (); -val t = (term_of o the o (parse thy)) "(sqrt(x)=1) is_ratequation_in x"; +val t = (Thm.term_of o the o (parse thy)) "(sqrt(x)=1) is_ratequation_in x"; val SOME (t_, _) = rewrite_set_ thy false RatEq_prls t; val result = term2str t_; if result <> "False" then error "rateq.sml: new behaviour 2:" else (); -val t = (term_of o the o (parse thy)) "(x=-1) is_ratequation_in x"; +val t = (Thm.term_of o the o (parse thy)) "(x=-1) is_ratequation_in x"; val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t; val result = term2str t_; if result <> "False" then error "rateq.sml: new behaviour 3:" else (); -val t = (term_of o the o (parse thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x"; +val t = (Thm.term_of o the o (parse thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x"; val SOME (t_,_) = rewrite_set_ thy false RatEq_prls t; val result = term2str t_; if result <> "True" then error "rateq.sml: new behaviour 4:" else (); diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/rational-old.sml --- a/test/Tools/isac/Knowledge/rational-old.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/rational-old.sml Mon Dec 07 14:10:59 2015 +0100 @@ -175,18 +175,18 @@ (* print("***** TERM2POLY-TESTS *****\n"); -val t0 = (term_of o the o (parse thy)) "3 * 4"; -val t1 = (term_of o the o (parse thy)) "27"; -val t11= (term_of o the o (parse thy)) "27 * c"; -val t2 = (term_of o the o (parse thy)) "b"; -val t23= (term_of o the o (parse thy)) "c^^^7"; -val t24= (term_of o the o (parse thy)) "5 * c^^^7"; -val t26= (term_of o the o (parse thy)) "a * b"; -val t3 = (term_of o the o (parse thy)) "2 + a"; -val t4 = (term_of o the o (parse thy)) "b + a"; -val t5 = (term_of o the o (parse thy)) "2 + a^^^3";*) -val t6 = (term_of o the o (parse thy)) "5*a^^^2*b^^^3*c+4*a^^^4*b+2*a*c"; -val t7 = (term_of o the o (parse thy)) "a-b"; +val t0 = (Thm.term_of o the o (parse thy)) "3 * 4"; +val t1 = (Thm.term_of o the o (parse thy)) "27"; +val t11= (Thm.term_of o the o (parse thy)) "27 * c"; +val t2 = (Thm.term_of o the o (parse thy)) "b"; +val t23= (Thm.term_of o the o (parse thy)) "c^^^7"; +val t24= (Thm.term_of o the o (parse thy)) "5 * c^^^7"; +val t26= (Thm.term_of o the o (parse thy)) "a * b"; +val t3 = (Thm.term_of o the o (parse thy)) "2 + a"; +val t4 = (Thm.term_of o the o (parse thy)) "b + a"; +val t5 = (Thm.term_of o the o (parse thy)) "2 + a^^^3";*) +val t6 = (Thm.term_of o the o (parse thy)) "5*a^^^2*b^^^3*c+4*a^^^4*b+2*a*c"; +val t7 = (Thm.term_of o the o (parse thy)) "a-b"; (* (the o term2poly) t0; (the o term2poly) t1; @@ -204,28 +204,28 @@ print("\n\n***** STEP_CANCEL_TESTS: *****\n"); (* -val term2 = (term_of o the o (parse thy)) " (9 * a^^^2 * b) /// (6 * a * c)"; +val term2 = (Thm.term_of o the o (parse thy)) " (9 * a^^^2 * b) /// (6 * a * c)"; val div2 = step_cancel term2; atomt div2; *) -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"; +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"; val div1 = step_cancel term1; -(*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");*) +(*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");*) -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) "; +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) "; val div2 = step_cancel term2; (*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");*) -val term3 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c) /// (1 * x * y * z) "; +val term3 = (Thm.term_of o the o (parse thy)) "(10 * a^^^2 * b * c) /// (1 * x * y * z) "; val div3 = step_cancel term3; -(*val mul1=(term_of o the o (parse thy)) "(5*a*b*c+4*a*b+2*a*c)"; -val mul2=(the (term2poly((term_of o the o (parse thy)) "13*a^^^2*b*c+7*a*b-19*a*b*c^^^2"))); -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"))); +(*val mul1=(Thm.term_of o the o (parse thy)) "(5*a*b*c+4*a*b+2*a*c)"; +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"))); +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"))); val t1=mv_mul(mul1,mul2,LEX_); val t2=mv_mul(mul3,mul2,LEX_); val div3=step_cancel t1 t2; @@ -237,7 +237,7 @@ val thy = Rational.thy; val rls = Prls {func=cancel}; -val t = (term_of o the o (parse thy)) +val t = (Thm.term_of o the o (parse thy)) "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2)"; val (t,asm) = the (rewrite_set_ thy eval_rls false rls t); @@ -261,9 +261,9 @@ val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); (* -val term2 = (term_of o the o (parse thy)) "(a^^^2 * b + 2 * a * b + b ) /// ( a^^^2 - 1 )"; +val term2 = (Thm.term_of o the o (parse thy)) "(a^^^2 * b + 2 * a * b + b ) /// ( a^^^2 - 1 )"; val div2 = direct_cancel term2; -val t = (term_of o the o (parse thy)) "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2) = 0";*) +val t = (Thm.term_of o the o (parse thy)) "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2) = 0";*) @@ -291,7 +291,7 @@ val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )"; val e186c = (the (rewrite_set thy' "rational_erls" false rls' e186c')) handle e => OldGoals.print_exn e; -val t = (term_of o the o (parse thy)) e186c'; +val t = (Thm.term_of o the o (parse thy)) e186c'; atomt t; print("\n\nexample 187:\n"); @@ -600,7 +600,7 @@ (* - val t = (term_of o the o (parse thy)) + val t = (Thm.term_of o the o (parse thy)) "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; val SOME (t',_) = factor_expanded_ thy t; term2str t'; @@ -616,7 +616,7 @@ the 'reverse-ruleset' cancel*) (*the term for which reverse rewriting is demonstrated*) - val t = (term_of o the o (parse thy)) + val t = (Thm.term_of o the o (parse thy)) "(9 - x ^^^ 2) / (9 + 6 * x + x ^^^ 2)"; val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc, next_rule=nex,normal_form=nor,...},...} = cancel; @@ -677,7 +677,7 @@ (*WN.11.9.02: the 'reverse-ruleset' cancel*) (*the term for which reverse rewriting is demonstrated*) - val t = (term_of o the o (parse thy)) + val t = (Thm.term_of o the o (parse thy)) "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))"; val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc, next_rule=nex,normal_form=nor,...},...} = cancel; @@ -731,8 +731,8 @@ OK Thm ("real_mult_div_cancel2","?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n")] -------- revset ---------------------------------------------------- - val t = (term_of o the o (parse thy)) "(-6) * x"; - val t = (term_of o the o (parse thy)) + val t = (Thm.term_of o the o (parse thy)) "(-6) * x"; + val t = (Thm.term_of o the o (parse thy)) "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))"; val thm = (mk_thm thy "(-6) * x = 2 * ((-3) * x)") handle e => OldGoals.print_exn e; @@ -744,38 +744,38 @@ (* SK: Testbeispiele --- WN kopiert Rational.ML -> rational.sml----- -val t1 = (term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))"; +val t1 = (Thm.term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))"; val SOME (t1',rest)= cancel_ thy t1; val SOME (t1'',_)= factor_out_gcd_ thy t1; print(term2str t1'^" + Einschr\"ankung: "^term2str (hd(rest))); term2str t1''; -val t1 = (term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))"; +val t1 = (Thm.term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))"; val SOME (t1',_)= cancel_ thy t1; val SOME (t1'',_)= factor_expanded_ thy t1; term2str t1'; term2str t1''; -val t2 = (term_of o the o (parse thy)) "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; +val t2 = (Thm.term_of o the o (parse thy)) "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; val SOME (t2',_) = add_fractions_ thy t2; val SOME (t2'',_) = common_nominators_ thy t2; term2str t2'; term2str t2''; -val t2 = (term_of o the o (parse thy)) "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))"; +val t2 = (Thm.term_of o the o (parse thy)) "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))"; val SOME (t2',_) = add_expanded_frac_ thy t2; val SOME (t2'',_) = common_expanded_nom_ thy t2; term2str t2'; term2str t2''; -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))"; +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))"; val SOME (t3',_) = common_nominators_ thy t3; val SOME (t3'',_) = add_fractions_ thy t3; (term2str t3'); (term2str t3''); -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))"; +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))"; val SOME (t3',_) = common_expanded_nom_ thy t3; val SOME (t3'',_) = add_expanded_frac_ thy t3; (term2str t3'); @@ -787,10 +787,10 @@ term2str t4; term2str (hd(t5));*) -(*val test1 = (term_of o the o (parse thy)) "1 - x^^^2 - 5 * x^^^5"; -val test2 = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^ 5"; -val test2 = (term_of o the o (parse thy)) "1 - x"; -val test2 = (term_of o the o (parse thy)) "1 + (-1) * x"; +(*val test1 = (Thm.term_of o the o (parse thy)) "1 - x^^^2 - 5 * x^^^5"; +val test2 = (Thm.term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^ 5"; +val test2 = (Thm.term_of o the o (parse thy)) "1 - x"; +val test2 = (Thm.term_of o the o (parse thy)) "1 + (-1) * x"; term2str(expanded2term(test1)); term2str(term2expanded(test2)); *) @@ -798,7 +798,7 @@ (* WN kopiert 16.10.02 Rational.ML -> rational.sml-----vvv---*) - val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)"; + val t=(Thm.term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)"; val SOME (t',_) = factout_ thy t; val SOME (t'',_) = cancel_ thy t; term2str t'; @@ -806,7 +806,7 @@ "(3 + x) * (3 - x) / ((3 - x) * (3 - x))"; "(3 + x) / (3 - x)"; - val t=(term_of o the o(parse thy)) + val t=(Thm.term_of o the o(parse thy)) "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)"; val SOME (t',_) = common_nominator_ thy t; val SOME (t'',_) = add_fraction_ thy t; @@ -816,7 +816,7 @@ "(4 + x) / (3 - x)"; (*WN.16.10.02 hinzugef"ugt -----vv---*) - val t=(term_of o the o(parse thy)) + val t=(Thm.term_of o the o(parse thy)) "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1"; val SOME (t',_) = common_nominator_ thy t; val SOME (t'',_) = add_fraction_ thy t; @@ -826,7 +826,7 @@ \1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; "6 / (3 - x)"; - val t=(term_of o the o(parse thy)) + val t=(Thm.term_of o the o(parse thy)) "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)"; val SOME (t',_) = common_nominator_ thy t; val SOME (t'',_) = add_fraction_ thy t; @@ -837,7 +837,7 @@ "6 / (3 - x)"; (*WN.16.10.02 hinzugef"ugt -----^^---*) - val t=(term_of o the o (parse thy)) + val t=(Thm.term_of o the o (parse thy)) "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)"; val SOME (t',_) = factout_ thy t; val SOME (t'',_) = cancel_ thy t; @@ -846,7 +846,7 @@ "(y + x) * (y - x) / ((y - x) * (y - x))"; "(y + x) / (y - x)"; - val t=(term_of o the o (parse thy)) + val t=(Thm.term_of o the o (parse thy)) "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)"; val SOME (t',_) = common_nominator_ thy t; val SOME (t'',_) = add_fraction_ thy t; @@ -857,7 +857,7 @@ "((-1) - x - y) / (x - y)"; (*WN.16.10.02 ^^^^^^^ Reihenfolge aus Angabe umgekehrt ?!*) - val t=(term_of o the o (parse thy)) + val t=(Thm.term_of o the o (parse thy)) "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)"; val SOME (t',_) = common_nominator_ thy t; val SOME (t'',_) = add_fraction_ thy t; @@ -868,7 +868,7 @@ "((-1) - y - x) / (y - x)"; (*WN.16.10.02 ^^^^^^^ lexicographische Ordnung ?!*) - val t=(term_of o the o (parse thy)) + val t=(Thm.term_of o the o (parse thy)) "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)"; val SOME (t',_) = norm_expanded_rat_ thy t; term2str t'; @@ -878,7 +878,7 @@ *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?!*) - val t=(term_of o the o (parse thy)) + val t=(Thm.term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)"; val SOME (t',_) = norm_expanded_rat_ thy t; term2str t'; @@ -888,7 +888,7 @@ *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?!*) - val t=(term_of o the o (parse thy)) + val t=(Thm.term_of o the o (parse thy)) "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)"; val SOME (t',_) = norm_expanded_rat_ thy t; val SOME (t'',_) = norm_rational_ thy t; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/rational.sml --- a/test/Tools/isac/Knowledge/rational.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Dec 07 14:10:59 2015 +0100 @@ -91,7 +91,7 @@ val vs = ["x","y","z"] (*precondition for [(c, es),...]: legth es = length vs*) ; -if term2str (term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5" +if term2str (Thm.term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5" then () else error "term_of_poly 1 changed"; "-------- integration lev.1 fun factout_p_ -----------------------------------"; @@ -721,8 +721,8 @@ ### Isabelle2009-2 for cancel_ (not cancel_p_): if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso string_of_thm thm = - (string_of_thm o make_thm o (cterm_of (@{theory "Isac"}))) - (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then () + (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac"}))) + (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2") then () else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; \---------------------------------------------------------------------------------------/*) @@ -740,8 +740,8 @@ (* find the next rule to apply *) val SOME (r as (Thm (str, thm))) = nex revsets t; if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso - string_of_thm thm = (string_of_thm o make_thm o (cterm_of (@{theory "Isac"}))) - (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then () + string_of_thm thm = (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac"}))) + (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2") then () else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; (*check the next rule*) @@ -1604,7 +1604,7 @@ "-------- fun eval_get_denominator -------------------------------------------"; "-------- fun eval_get_denominator -------------------------------------------"; val thy = @{theory Isac}; -val t = term_of (the (parse thy "get_denominator ((a +x)/b)")); +val t = Thm.term_of (the (parse thy "get_denominator ((a +x)/b)")); val SOME (_, t') = eval_get_denominator "" 0 t thy; if term2str t' = "get_denominator ((a + x) / b) = b" then () else error "get_denominator ((a + x) / b) = b" diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/rlang.sml --- a/test/Tools/isac/Knowledge/rlang.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/rlang.sml Mon Dec 07 14:10:59 2015 +0100 @@ -206,9 +206,9 @@ | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []"; (*WN---v *) -val bdv= (term_of o the o (parse thy)) "bdv"; -val v = (term_of o the o (parse thy)) "x"; -val t = (term_of o the o (parse thy)) "3 * x / 5"; +val bdv= (Thm.term_of o the o (parse thy)) "bdv"; +val v = (Thm.term_of o the o (parse thy)) "x"; +val t = (Thm.term_of o the o (parse thy)) "3 * x / 5"; val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true [(bdv, v)] make_ratpoly_in t; if term2str t' = "3 / 5 * x" then () else error "rlang.sml: 1"; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/rooteq.sml --- a/test/Tools/isac/Knowledge/rooteq.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/rooteq.sml Mon Dec 07 14:10:59 2015 +0100 @@ -18,62 +18,62 @@ (*=== inhibit exn ?============================================================= -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.False" then error "rooteq.sml: new behaviour:" else (); -val t = (term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x"; +val t = (Thm.term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x"; val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t; val result = term2str t_; if result <> "HOL.True" then error "rooteq.sml: new behaviour:" else (); diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/Knowledge/rootrateq.sml --- a/test/Tools/isac/Knowledge/rootrateq.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Mon Dec 07 14:10:59 2015 +0100 @@ -18,37 +18,37 @@ "------------ tests on predicates -------------------------------"; "------------ tests on predicates -------------------------------"; "------------ tests on predicates -------------------------------"; -val t1 = (term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x"; +val t1 = (Thm.term_of o the o (parse thy)) "(-8 - sqrt(x) + x^^^2) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (term2str t) = "False" then () else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in"; -val t1 = (term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x"; +val t1 = (Thm.term_of o the o (parse thy)) "(1/x) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (term2str t) = "False" then () else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in"; -val t1 = (term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; +val t1 = (Thm.term_of o the o (parse thy)) "(1/sqrt(x)) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (term2str t) = "False" then () else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in"; -val t1 = (term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; +val t1 = (Thm.term_of o the o (parse thy)) "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (term2str t) = "True" then () else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in"; -val t1 = (term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; +val t1 = (Thm.term_of o the o (parse thy)) "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (term2str t) = "True" then () else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in"; -val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; +val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (term2str t) = "True" then () else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in"; -val t1 = (term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; +val t1 = (Thm.term_of o the o (parse thy)) "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x"; val SOME (t,_) = rewrite_set_ @{theory "RootRatEq"} false RootRatEq_prls t1; if (term2str t) = "True" then () else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in"; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/OLDTESTS/root-equ.sml --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Mon Dec 07 14:10:59 2015 +0100 @@ -30,7 +30,7 @@ (* -> val t = (term_of o the o (parse thy)) "#2^^^#3"; +> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3"; > val eval_fn = the (assoc (!eval_list, "pow")); > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; > Syntax.string_of_term (thy2ctxt thy) t'; @@ -120,7 +120,7 @@ parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}"; (* 31.1.00 val tag__forms = chktyps thy (formals, givens); -map ((atomty) o term_of) tag__forms; *) +map ((atomty) o Thm.term_of) tag__forms; *) " --- subproblem 2: linear-equation --- "; val origin = ["x + 4 = (0::real)","x::real"]; @@ -135,14 +135,14 @@ val givens = map (the o (parse thy)) given; val tag__forms = chktyps thy (formals, givens); -map ((atomty) o term_of) tag__forms; +map ((atomty) o Thm.term_of) tag__forms; " _________________ rewrite_ x+4_________________ "; " _________________ rewrite_ x+4_________________ "; " _________________ rewrite_ x+4_________________ "; -val t = (term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; +val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; val thm = num_str @{thm square_equation_left}; val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t); val rls = Test_simplify; @@ -210,8 +210,8 @@ " _________________ rewrite x=4_________________ "; (* rewrite thy' "tless_true" "tval_rls" true (num_str @{thm rbinom_power_2}) ct; -atomty ((#prop o rep_thm) (!tthm)); -atomty (term_of (!tct)); +atomty ((#prop o Thm.rep_thm) (!tthm)); +atomty (Thm.term_of (!tct)); *) val thy' = "Test"; val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; @@ -385,7 +385,7 @@ *) (* -val t = (term_of o the o (parse thy)) "solutions (L::real set)"; +val t = (Thm.term_of o the o (parse thy)) "solutions (L::real set)"; atomty t; *) @@ -573,7 +573,7 @@ -val ttt = (term_of o the o (parse Test.thy)) +val ttt = (Thm.term_of o the o (parse Test.thy)) "Let (((While contains_root e_e Do\ \Rewrite square_equation_left True @@\ \Try (Rewrite_Set Test_simplify False) @@\ diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/OLDTESTS/script.sml --- a/test/Tools/isac/OLDTESTS/script.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/OLDTESTS/script.sml Mon Dec 07 14:10:59 2015 +0100 @@ -74,7 +74,7 @@ \ [BOOL e_2, REAL v_2])\ \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; -val ags = map (term_of o the o (parse DiffApp.thy)) +val ags = map (Thm.term_of o the o (parse DiffApp.thy)) ["A::real", "alpha::real", "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"]; val ll = [](*:loc_*); @@ -156,7 +156,7 @@ (*#####################################################--------11.5.02 "################ Solve_root_equation #################"; (*#####################################################*) -val sc = (term_of o the o (parse Test.thy)) +val sc = (Thm.term_of o the o (parse Test.thy)) "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\ \ (let e_e = Rewrite square_equation_left True eq_; \ \ e_e = Rewrite_Set Test_simplify False e_; \ @@ -172,7 +172,7 @@ \ e_e = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\ \ e_e = Rewrite_Set Test_simplify False e_e \ \ in [e_::bool])"; -val ags = map (term_of o the o (parse Test.thy)) +val ags = map (Thm.term_of o the o (parse Test.thy)) ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"]; val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", @@ -248,7 +248,7 @@ " --- test100: nxt_tac order------------------------------------ "; val scr as (Prog sc) = Prog (((inst_abs Test.thy) - o term_of o the o (parse thy)) + o Thm.term_of o the o (parse thy)) "Script Testeq (e_e::bool) = \ \(While (contains_root e_e) Do \ \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ @@ -266,10 +266,10 @@ val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*) val (p,_,_,_,_,pt) = me nxt p c pt; val p = ([1],Res):pos'; -val eq_ = (term_of o the o (parse thy))"e_::bool"; +val eq_ = (Thm.term_of o the o (parse thy))"e_::bool"; val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; -val ve0_= (term_of o the o (parse thy)) ct; +val ve0_= (Thm.term_of o the o (parse thy)) ct; val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)], e_term,e_term,Safe)), ([],(User', [], [], e_term, e_term,Sundef))]:ets; @@ -282,14 +282,14 @@ val scr as (Prog sc) = - Prog (((inst_abs Test.thy) o term_of o the o (parse thy)) + Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) "Script Testterm (g_::real) = (Calculate cancel g_)"); (* val scr as (Prog sc) = - Prog (((inst_abs Test.thy) o term_of o the o (parse thy)) + Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) "Script Testterm (g_::real) = (Calculate power g_)"); val scr as (Prog sc) = - Prog (((inst_abs Test.thy) o term_of o the o (parse thy)) + Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy)) "Script Testterm (g_::real) = (Calculate pow g_)"); ..............................................................*) writeln diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/OLDTESTS/script_if.sml --- a/test/Tools/isac/OLDTESTS/script_if.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Mon Dec 07 14:10:59 2015 +0100 @@ -9,35 +9,35 @@ (*---------------- 25.7.02 ---------------------*) val thy = (theory "Isac"); -val t = (term_of o the o (parse thy)) "contains_root (sqrt(x)=1)"; +val t = (Thm.term_of o the o (parse thy)) "contains_root (sqrt(x)=1)"; val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy; -val t = (term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x"; +val t = (Thm.term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x"; val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; (*--- -val v = (term_of o the o (parse thy)) "x"; -val t = (term_of o the o (parse thy)) "sqrt(#3+#4*x)"; +val v = (Thm.term_of o the o (parse thy)) "x"; +val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*x)"; scan t v; -val t = (term_of o the o (parse thy)) "sqrt(#3+#4*a)"; +val t = (Thm.term_of o the o (parse thy)) "sqrt(#3+#4*a)"; scan t v; -val t = (term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)"; +val t = (Thm.term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)"; scan t v; -val t = (term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)"; +val t = (Thm.term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)"; scan t v; ---*) -val t = (term_of o the o (parse thy)) +val t = (Thm.term_of o the o (parse thy)) "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x"; val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; -val t = (term_of o the o (parse thy)) +val t = (Thm.term_of o the o (parse thy)) "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x"; val SOME(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; -val t = (term_of o the o (parse Test.thy)) +val t = (Thm.term_of o the o (parse Test.thy)) "is_rootequation_in (sqrt(x)=1) x"; atomty t; -val t = (term_of o the o (parse (theory "Isac"))) +val t = (Thm.term_of o the o (parse (theory "Isac"))) "is_rootequation_in (sqrt(x)=1) x"; atomty t; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/OLDTESTS/scriptnew.sml --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Mon Dec 07 14:10:59 2015 +0100 @@ -483,7 +483,7 @@ (*GoOn.5.03. script with Map, Subst (biquadr.equ.) -val scr = Prog (((inst_abs thy) o term_of o the o (parse thy)) +val scr = Prog (((inst_abs thy) o Thm.term_of o the o (parse thy)) "Script Biquadrat_poly (e_e::bool) (v_::real) = \ \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \ \ L_0_ = (SubProblem (PolyEq_,[univariate,equation], [no_met]) \ diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/ProgLang/calculate.sml --- a/test/Tools/isac/ProgLang/calculate.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/ProgLang/calculate.sml Mon Dec 07 14:10:59 2015 +0100 @@ -32,7 +32,7 @@ val cal = snd (assoc_calc' thy "is_polyexp"); val t = @{term "(x / x) is_polyexp"}; val SOME (thmID, thm) = get_calculation_ thy cal t; -(HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop") +(HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop") handle TERM _ => error "calculate.sml: get_calculation_ must return Trueprop"; @@ -41,12 +41,12 @@ "----------- fun calculate_ -----------------------------"; val thy = @{theory "Test"}; "===== test 1"; -val t = (term_of o the o (parse thy)) "1+2"; +val t = (Thm.term_of o the o (parse thy)) "1+2"; val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; term2str (prop_of thm) = "1 + 2 = 3"; "===== test 2"; -val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2"; +val t = (Thm.term_of o the o (parse thy)) "((1+2)*4/3)^^^2"; val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; if term2str t = "(3 * 4 / 3) ^^^ 2" then () @@ -131,7 +131,7 @@ (*--------------(2): does divide work in Test_simplify ?: ------*) val thy = @{theory Test}; - val t = (term_of o the o (parse thy)) "6 / 2"; + val t = (Thm.term_of o the o (parse thy)) "6 / 2"; val rls = Test_simplify; val (t,_) = the (rewrite_set_ thy false rls t); (*val t = Free ("3","Real.real") : term*) @@ -145,7 +145,7 @@ (*--------------(3): is_const works ?: -------------------------------------*) - val t = (term_of o the o (parse @{theory Test})) "2 is_const"; + val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const"; atomty t; rewrite_set_ @{theory Test} false tval_rls t; (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*) @@ -161,7 +161,7 @@ (*-------------- eval_cancel works: *) trace_rewrite:=false; val thy = @{theory Test}; - val t = (term_of o the o (parse thy)) "(-4) / 2"; + val t = (Thm.term_of o the o (parse thy)) "(-4) / 2"; val SOME (_, t) = eval_cancel "xxx" "Fields.inverse_class.divide" t thy; @@ -282,7 +282,7 @@ "----------- Atools.pow Power.power_class.power ---------"; "----------- Atools.pow Power.power_class.power ---------"; "----------- Atools.pow Power.power_class.power ---------"; -val t = (term_of o the o (parseold thy)) "1 ^ aaa"; +val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa"; atomty t; (*** ------------- *** Const ( Nat.power, ['a, nat] => 'a) @@ -302,17 +302,17 @@ " ================= calculate.sml: calculate_ 2002 =================== "; val thy = @{theory Test}; -val t = (term_of o the o (parse thy)) "12 / 3"; +val t = (Thm.term_of o the o (parse thy)) "12 / 3"; val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; "12 / 3 = 4"; val thy = @{theory Test}; -val t = (term_of o the o (parse thy)) "4 ^^^ 2"; +val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2"; val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; "4 ^ 2 = 16"; - val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; + val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; "1 + 2 = 3"; val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; @@ -337,7 +337,7 @@ else (); (*13.9.02 *** calc: operator = pow not defined*) - val t = (term_of o the o (parse thy)) "3^^^2"; + val t = (Thm.term_of o the o (parse thy)) "3^^^2"; val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"POWER"))) t; (*** calc: operator = pow not defined*) diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/ProgLang/listC.sml --- a/test/Tools/isac/ProgLang/listC.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/ProgLang/listC.sml Mon Dec 07 14:10:59 2015 +0100 @@ -21,7 +21,7 @@ val t = str2term "NTH 1 [a,b,c,d,e]"; atomty t; -val thm = (#prop o rep_thm o num_str) @{thm NTH_NIL}; +val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_NIL}; atomty thm; val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_NIL}) t; if term2str t' = "a" then () @@ -32,7 +32,7 @@ (Const ("List.list.Cons", _) $ Free ("b", _) $ (Const _ $ Free _ $ (Const _ $ Free _ $ (Const _ $ Free _ $ Const _))))) = t; atomty t; -val thm = (#prop o rep_thm o num_str) @{thm NTH_CONS}; +val thm = (#prop o Thm.rep_thm o num_str) @{thm NTH_CONS}; atomty thm; val SOME (t', _) = rewrite_ thy dummy_ord list_rls false (num_str @{thm NTH_CONS}) t; if term2str t' = "NTH (3 + -1) [b, c, d, e]" then () diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/ProgLang/rewrite.sml --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/ProgLang/rewrite.sml Mon Dec 07 14:10:59 2015 +0100 @@ -36,10 +36,10 @@ val thy = @{theory Complex_Main}; val ctxt = @{context}; val thm = @{thm add.commute}; -val t = (term_of o the) (parse thy "((r + u) + t) + s"); +val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s"); "----- from old: fun rewrite__"; val bdv = []; -val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm); +val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm); "----- from old: and rew_sub"; val (LHS,RHS) = (dest_equals' o strip_trueprop o Logic.strip_imp_concl) r; @@ -162,11 +162,11 @@ "----------- step through 'and rew_sub': ----------------"; (*and make asms without Trueprop, beginning with the result:*) val tm = @{term "x*y / y::real"}; -val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm; +val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (Thm.prop_of thm) tm; (*show_types := false;*) "----- evaluate arguments"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = - (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm); + (thy, 0, [], dummy_ord, e_rls, true, [], (Thm.prop_of thm), tm); "----- step 1: LHS, RHS of rule"; val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r; @@ -315,7 +315,7 @@ val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t; (*t' = t''; (*false because of further rewrites in t'*)*) "----- rew_sub --------------------------------"; -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t; +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t; (*t'' = t'''; (*true*)*) "----- rewrite_set_ erls --------------------------------"; val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"}; @@ -334,7 +334,7 @@ val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t; (*t' = t''; (*false because of further rewrites in t'*)*) writeln "----- rew_sub --------------------------------"; -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t; +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t; (*t'' = t'''; (*true*)*) writeln "----- rewrite_set_ erls --------------------------------"; val cond = @{term "(x / x ^^^ 2)"}; @@ -502,7 +502,7 @@ "----------- 2011 thms with axclasses -------------------"; "----------- 2011 thms with axclasses -------------------"; val thm = num_str @{thm divide_1}; -val prop = prop_of thm; +val prop = Thm.prop_of thm; atomty prop; (*Type 'a*) val t = str2term "(2*x)/1"; (*Type real*) diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/ProgLang/termC.sml --- a/test/Tools/isac/ProgLang/termC.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/ProgLang/termC.sml Mon Dec 07 14:10:59 2015 +0100 @@ -169,17 +169,17 @@ "----------- inst_bdv -----------------------------------"; "----------- inst_bdv -----------------------------------"; "----------- inst_bdv -----------------------------------"; - if (term2str o prop_of o num_str) @{thm d1_isolate_add2} = + if (term2str o Thm.prop_of o num_str) @{thm d1_isolate_add2} = "~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)" then () else error "termC.sml d1_isolate_add2"; val subst = [(str2term "bdv", str2term "x")]; - val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2}); + val t = (norm o #prop o Thm.rep_thm) (num_str @{thm d1_isolate_add2}); val t' = inst_bdv subst t; if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then () else error "termC.sml inst_bdv 1"; -if (term2str o prop_of o num_str) @{thm separate_bdvs_add} = +if (term2str o Thm.prop_of o num_str) @{thm separate_bdvs_add} = "[] from [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n==>" ^ " (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then () else error "termC.sml separate_bdvs_add"; @@ -190,7 +190,7 @@ (str2term "bdv_2", str2term "c_2"), (str2term "bdv_3", str2term "c_3"), (str2term "bdv_4", str2term "c_4")]; -val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add}); +val t = (norm o #prop o Thm.rep_thm) (num_str @{thm separate_bdvs_add}); val t' = inst_bdv subst t; if term2str t' = "[] from [c, c_2, c_3, c_4] occur_exactly_in ?a\n\ @@ -218,8 +218,8 @@ "----------- Pattern.match ------------------------------"; "----------- Pattern.match ------------------------------"; "----------- Pattern.match ------------------------------"; - val t = (term_of o the o (parse thy)) "3 * x^^^2 = (1::real)"; - val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)"; + val t = (Thm.term_of o the o (parse thy)) "3 * x^^^2 = (1::real)"; + val pat = (free2var o Thm.term_of o the o (parse thy)) "a * b^^^2 = (c::real)"; (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*) val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty); default_print_depth 3; (*999*) insts; @@ -329,7 +329,7 @@ val t = (Syntax.read_term_global thy str); val t = numbers_to_string (Syntax.read_term_global thy str); val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str); - cterm_of thy t; + Thm.global_cterm_of thy t; val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed"; "===== fun parse_patt caused error in fun T_a2real ==="; @@ -344,7 +344,7 @@ val t = (Syntax.read_term_global thy str); val t = numbers_to_string (Syntax.read_term_global thy str); val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str); - cterm_of thy t; + Thm.global_cterm_of thy t; val t = (the (parse thy str)) handle _ => error "termC.sml parsing 'x + 2*z' failed"; "===== fun parse_patt caused error in fun T_a2real ==="; diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/calcelems.sml --- a/test/Tools/isac/calcelems.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/calcelems.sml Mon Dec 07 14:10:59 2015 +0100 @@ -81,7 +81,7 @@ fun parse thy str = (let val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str) - in SOME (cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*) + in SOME (Thm.global_cterm_of thy t) end) (*FIXXXXME 10.8.02: return term !!!*) handle _ => NONE; *) diff -r 2b26acbd130c -r c477d0f79ab9 test/Tools/isac/xmlsrc/thy-hierarchy.sml --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Dec 07 11:32:12 2015 +0100 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Dec 07 14:10:59 2015 +0100 @@ -17,7 +17,7 @@ "----------- ### thes2file ... Exception- Match raised -----------"; "----------- search for data error in thes2file ------------------"; "----------- thes2file: thy_containing_rls : rls '...' not in ! --"; -"----------- fun make_thm ----------------------------------------"; +"----------- fun Thm.make_thm ------------------------------------"; "----------- correct theIDs for e_rls ----------------------------"; "----------- correct theIDs for list_rls -------------------------"; "----------- fun revert_sym --------------------------------------"; @@ -121,12 +121,12 @@ ; thydata2xml (theID, thydata); -"----------- fun make_thm ----------------------------------------"; -"----------- fun make_thm ----------------------------------------"; -"----------- fun make_thm ----------------------------------------"; -"~~~~~ fun make_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) = +"----------- fun Thm.make_thm ------------------------------------"; +"----------- fun Thm.make_thm ------------------------------------"; +"----------- fun Thm.make_thm ------------------------------------"; +"~~~~~ fun Thm.make_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) = (@{theory "Biegelinie"}, "IsacKnowledge", - ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft}), + ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}), ["Walther Neuper 2005 supported by a grant from NMI Austria"]); val guh = thm2guh (part, theory2thyID thy) thmID val theID = guh2theID guh; @@ -196,7 +196,7 @@ |> map (revert_sym thy) (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"), Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*) - |> map (fn Thm (thmID, thm) => (thmID, prop_of thm)) + |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm)) (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \ prop") $ ..., ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*) |> gen_distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);