1.1 --- a/src/Tools/isac/CLEANUP Tue Aug 31 16:00:13 2010 +0200
1.2 +++ b/src/Tools/isac/CLEANUP Tue Aug 31 16:38:22 2010 +0200
1.3 @@ -1,5 +1,6 @@
1.4 rm *~
1.5 rm *.tar*
1.6 +rm *.orig
1.7 cd ProgLang
1.8 rm *~
1.9 rm #*
2.1 --- a/src/Tools/isac/Knowledge/Atools.thy Tue Aug 31 16:00:13 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Aug 31 16:38:22 2010 +0200
2.3 @@ -6,7 +6,14 @@
2.4 10 20 30 40 50 60 70 80
2.5 *)
2.6
2.7 -theory Atools imports Descript begin
2.8 +theory Atools imports Descript
2.9 +uses ("../Interpret/mstools.sml")
2.10 + ("../Interpret/ctree.sml")
2.11 + ("../Interpret/ptyps.sml") (*^^^ all for: fun prep_pbt, fun store_pbt*)
2.12 +begin
2.13 +use "../Interpret/mstools.sml"
2.14 +use "../Interpret/ctree.sml"
2.15 +use "../Interpret/ptyps.sml"
2.16
2.17 consts
2.18
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue Aug 31 16:00:13 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Aug 31 16:38:22 2010 +0200
3.3 @@ -228,7 +228,7 @@
3.4 ],
3.5 scr = EmptyScr};
3.6 ruleset' :=
3.7 -overwritelthy thy (!ruleset',
3.8 +overwritelthy @{theory} (!ruleset',
3.9 [("diff_rules", prep_rls norm_diff),
3.10 ("norm_diff", prep_rls norm_diff),
3.11 ("diff_conv", prep_rls diff_conv),
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Tue Aug 31 16:00:13 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Aug 31 16:38:22 2010 +0200
4.3 @@ -74,7 +74,7 @@
4.4 scr = Script ((term_of o the o (parse thy))
4.5 "empty_script")
4.6 }:rls);
4.7 -ruleset' := overwritelthy thy
4.8 +ruleset' := overwritelthy @{theory}
4.9 (!ruleset',
4.10 [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*)
4.11 ]);
4.12 @@ -244,7 +244,7 @@
4.13 [Thm ("filterVar_Const", num_str @{filterVar_Const),
4.14 Thm ("filterVar_Nil", num_str @{filterVar_Nil)
4.15 ];
4.16 -ruleset' := overwritelthy thy (!ruleset',
4.17 +ruleset' := overwritelthy @{theory} (!ruleset',
4.18 [("list_rls",list_rls)
4.19 ]);
4.20 *}
5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Aug 31 16:00:13 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Aug 31 16:38:22 2010 +0200
5.3 @@ -393,7 +393,7 @@
5.4 scr = EmptyScr};
5.5
5.6 ruleset' :=
5.7 -overwritelthy thy
5.8 +overwritelthy @{theory}
5.9 (!ruleset',
5.10 [("simplify_System_parenthesized", prep_rls simplify_System_parenthesized),
5.11 ("simplify_System", prep_rls simplify_System),
6.1 --- a/src/Tools/isac/Knowledge/Equation.thy Tue Aug 31 16:00:13 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Tue Aug 31 16:38:22 2010 +0200
6.3 @@ -32,7 +32,7 @@
6.4 append_rls "univariate_equation_prls" e_rls
6.5 [Calc ("Tools.matches",eval_matches "")];
6.6 ruleset' :=
6.7 -overwritelthy thy (!ruleset',
6.8 +overwritelthy @{theory} (!ruleset',
6.9 [("univariate_equation_prls",
6.10 prep_rls univariate_equation_prls)]);
6.11
7.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Tue Aug 31 16:00:13 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Tue Aug 31 16:38:22 2010 +0200
7.3 @@ -98,7 +98,7 @@
7.4 "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
7.5 ));
7.6
7.7 -ruleset' := overwritelthy thy (!ruleset',
7.8 +ruleset' := overwritelthy @{theory} (!ruleset',
7.9 [(*("ins_sort",ins_sort) overwrites a Isa fun!!*)
7.10 ]:(string * rls) list);
7.11 *}
8.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Tue Aug 31 16:00:13 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Aug 31 16:38:22 2010 +0200
8.3 @@ -316,7 +316,7 @@
8.4 ],
8.5 scr = EmptyScr};
8.6 ruleset' :=
8.7 -overwritelthy thy (!ruleset',
8.8 +overwritelthy @{theory} (!ruleset',
8.9 [("integration_rules", prep_rls integration_rules),
8.10 ("add_new_c", prep_rls add_new_c),
8.11 ("simplify_Integral", prep_rls simplify_Integral),
9.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Tue Aug 31 16:00:13 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Aug 31 16:38:22 2010 +0200
9.3 @@ -69,7 +69,7 @@
9.4 *)
9.5 ];
9.6
9.7 -ruleset' := overwritelthy thy (!ruleset',
9.8 +ruleset' := overwritelthy @{theory} (!ruleset',
9.9 [("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*)
9.10 ]);
9.11
9.12 @@ -93,7 +93,7 @@
9.13 ],
9.14 scr = Script ((term_of o the o (parse thy)) "empty_script")
9.15 }:rls);
9.16 -ruleset' := overwritelthy thy (!ruleset',
9.17 +ruleset' := overwritelthy @{theory} (!ruleset',
9.18 [("LinPoly_simplify",LinPoly_simplify)]);
9.19
9.20 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
9.21 @@ -114,7 +114,7 @@
9.22 ],
9.23 scr = Script ((term_of o the o (parse thy)) "empty_script")
9.24 }:rls);
9.25 -ruleset' := overwritelthy thy (!ruleset',
9.26 +ruleset' := overwritelthy @{theory} (!ruleset',
9.27 [("LinEq_simplify",LinEq_simplify)]);
9.28
9.29 (*----------------------------- problem types --------------------------------*)
10.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Aug 31 16:00:13 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Aug 31 16:38:22 2010 +0200
10.3 @@ -1532,7 +1532,7 @@
10.4 scr = EmptyScr}:rls;
10.5
10.6 ruleset' :=
10.7 -overwritelthy thy (!ruleset',
10.8 +overwritelthy @{theory} (!ruleset',
10.9 [("norm_Poly", prep_rls norm_Poly),
10.10 ("Poly_erls",Poly_erls)(*FIXXXME:del with rls.rls'*),
10.11 ("expand", prep_rls expand),
10.12 @@ -1581,7 +1581,7 @@
10.13 store_pbt
10.14 (prep_pbt (theory "Poly") "pbl_simp_poly" [] e_pblID
10.15 (["polynomial","simplification"],
10.16 - [("#Given" ,["term t_"]),
10.17 + [("#Given" ,["TERM t_"]),
10.18 ("#Where" ,["t_ is_polyexp"]),
10.19 ("#Find" ,["normalform n_"])
10.20 ],
10.21 @@ -1596,7 +1596,7 @@
10.22 store_met
10.23 (prep_met (theory "Poly") "met_simp_poly" [] e_metID
10.24 (["simplification","for_polynomials"],
10.25 - [("#Given" ,["term t_"]),
10.26 + [("#Given" ,["TERM t_"]),
10.27 ("#Where" ,["t_ is_polyexp"]),
10.28 ("#Find" ,["normalform n_"])
10.29 ],
11.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Aug 31 16:00:13 2010 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Aug 31 16:38:22 2010 +0200
11.3 @@ -467,7 +467,7 @@
11.4 scr = Script ((term_of o the o (parse thy)) "empty_script")
11.5 }:rls);
11.6
11.7 -ruleset' := overwritelthy thy (!ruleset',
11.8 +ruleset' := overwritelthy @{theory} (!ruleset',
11.9 [("cancel_leading_coeff",cancel_leading_coeff),
11.10 ("complete_square",complete_square),
11.11 ("PolyEq_erls",PolyEq_erls),(*FIXXXME:del with rls.rls'*)
11.12 @@ -806,7 +806,7 @@
11.13 }:rls);
11.14
11.15 ruleset' :=
11.16 -overwritelthy thy
11.17 +overwritelthy @{theory}
11.18 (!ruleset',
11.19 [("d0_polyeq_simplify", d0_polyeq_simplify),
11.20 ("d1_polyeq_simplify", d1_polyeq_simplify),
11.21 @@ -1439,7 +1439,7 @@
11.22 scr = EmptyScr}:rls);
11.23
11.24
11.25 -ruleset' := overwritelthy thy (!ruleset',
11.26 +ruleset' := overwritelthy @{theory} (!ruleset',
11.27 [("order_add_mult_in", order_add_mult_in),
11.28 ("collect_bdv", collect_bdv),
11.29 ("make_polynomial_in", make_polynomial_in),
12.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Aug 31 16:00:13 2010 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Aug 31 16:38:22 2010 +0200
12.3 @@ -384,7 +384,7 @@
12.4 ];
12.5
12.6 ruleset' :=
12.7 -overwritelthy thy (!ruleset',
12.8 +overwritelthy @{theory} (!ruleset',
12.9 [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
12.10 ("fasse_zusammen", prep_rls fasse_zusammen),
12.11 ("verschoenere", prep_rls verschoenere),
12.12 @@ -404,7 +404,7 @@
12.13 store_pbt
12.14 (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_minus" [] e_pblID
12.15 (["plus_minus","polynom","vereinfachen"],
12.16 - [("#Given" ,["term t_"]),
12.17 + [("#Given" ,["TERM t_"]),
12.18 ("#Where" ,["t_ is_polyexp",
12.19 "Not (matchsub (?a + (?b + ?c)) t_ | " ^
12.20 " matchsub (?a + (?b - ?c)) t_ | " ^
12.21 @@ -433,7 +433,7 @@
12.22 store_pbt
12.23 (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_klammer" [] e_pblID
12.24 (["klammer","polynom","vereinfachen"],
12.25 - [("#Given" ,["term t_"]),
12.26 + [("#Given" ,["TERM t_"]),
12.27 ("#Where" ,["t_ is_polyexp",
12.28 "Not (matchsub (?a * (?b + ?c)) t_ | " ^
12.29 " matchsub (?a * (?b - ?c)) t_ | " ^
12.30 @@ -457,7 +457,7 @@
12.31 store_pbt
12.32 (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_klammer_mal" [] e_pblID
12.33 (["binom_klammer","polynom","vereinfachen"],
12.34 - [("#Given" ,["term t_"]),
12.35 + [("#Given" ,["TERM t_"]),
12.36 ("#Where" ,["t_ is_polyexp"]),
12.37 ("#Find" ,["normalform n_"])
12.38 ],
12.39 @@ -503,7 +503,7 @@
12.40 store_met
12.41 (prep_met (theory "PolyMinus") "met_simp_poly_minus" [] e_metID
12.42 (["simplification","for_polynomials","with_minus"],
12.43 - [("#Given" ,["term t_"]),
12.44 + [("#Given" ,["TERM t_"]),
12.45 ("#Where" ,["t_ is_polyexp",
12.46 "Not (matchsub (?a + (?b + ?c)) t_ | " ^
12.47 " matchsub (?a + (?b - ?c)) t_ | " ^
12.48 @@ -533,7 +533,7 @@
12.49 store_met
12.50 (prep_met (theory "PolyMinus") "met_simp_poly_parenth" [] e_metID
12.51 (["simplification","for_polynomials","with_parentheses"],
12.52 - [("#Given" ,["term t_"]),
12.53 + [("#Given" ,["TERM t_"]),
12.54 ("#Where" ,["t_ is_polyexp"]),
12.55 ("#Find" ,["normalform n_"])
12.56 ],
12.57 @@ -552,7 +552,7 @@
12.58 store_met
12.59 (prep_met (theory "PolyMinus") "met_simp_poly_parenth_mult" [] e_metID
12.60 (["simplification","for_polynomials","with_parentheses_mult"],
12.61 - [("#Given" ,["term t_"]),
12.62 + [("#Given" ,["TERM t_"]),
12.63 ("#Where" ,["t_ is_polyexp"]),
12.64 ("#Find" ,["normalform n_"])
12.65 ],
13.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Tue Aug 31 16:00:13 2010 +0200
13.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Aug 31 16:38:22 2010 +0200
13.3 @@ -106,7 +106,7 @@
13.4 [Thm ("and_commute",num_str @{and_commute), (*WN: ein Hack*)
13.5 Thm ("or_commute",num_str @{or_commute) (*WN: ein Hack*)
13.6 ];
13.7 -ruleset' := overwritelthy thy (!ruleset',
13.8 +ruleset' := overwritelthy @{theory} (!ruleset',
13.9 [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
13.10 ]);
13.11
13.12 @@ -138,7 +138,7 @@
13.13 ],
13.14 scr = Script ((term_of o the o (parse thy)) "empty_script")
13.15 }:rls);
13.16 -ruleset' := overwritelthy thy (!ruleset',
13.17 +ruleset' := overwritelthy @{theory} (!ruleset',
13.18 [("RatEq_eliminate",RatEq_eliminate)
13.19 ]);
13.20
13.21 @@ -165,7 +165,7 @@
13.22 ],
13.23 scr = Script ((term_of o the o (parse thy)) "empty_script")
13.24 }:rls);
13.25 -ruleset' := overwritelthy thy (!ruleset',
13.26 +ruleset' := overwritelthy @{theory} (!ruleset',
13.27 [("RatEq_simplify",RatEq_simplify)
13.28 ]);
13.29
14.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Aug 31 16:00:13 2010 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Aug 31 16:38:22 2010 +0200
14.3 @@ -3761,7 +3761,7 @@
14.4 (* ------------------------------------------------------------------ *)
14.5
14.6
14.7 -ruleset' := overwritelthy thy (!ruleset',
14.8 +ruleset' := overwritelthy @{theory} (!ruleset',
14.9 [("calculate_Rational", calculate_Rational),
14.10 ("calc_rat_erls",calc_rat_erls),
14.11 ("rational_erls", rational_erls),
14.12 @@ -3794,7 +3794,7 @@
14.13 store_pbt
14.14 (prep_pbt (theory "Rational") "pbl_simp_rat" [] e_pblID
14.15 (["rational","simplification"],
14.16 - [("#Given" ,["term t_"]),
14.17 + [("#Given" ,["TERM t_"]),
14.18 ("#Where" ,["t_ is_ratpolyexp"]),
14.19 ("#Find" ,["normalform n_"])
14.20 ],
14.21 @@ -3809,7 +3809,7 @@
14.22 store_met
14.23 (prep_met (theory "Rational") "met_simp_rat" [] e_metID
14.24 (["simplification","of_rationals"],
14.25 - [("#Given" ,["term t_"]),
14.26 + [("#Given" ,["TERM t_"]),
14.27 ("#Where" ,["t_ is_ratpolyexp"]),
14.28 ("#Find" ,["normalform n_"])
14.29 ],
15.1 --- a/src/Tools/isac/Knowledge/Root.thy Tue Aug 31 16:00:13 2010 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Root.thy Tue Aug 31 16:38:22 2010 +0200
15.3 @@ -185,7 +185,7 @@
15.4 Calc ("op =",eval_equal "#equal_")
15.5 ];
15.6
15.7 -ruleset' := overwritelthy thy (!ruleset',
15.8 +ruleset' := overwritelthy @{theory} (!ruleset',
15.9 [("Root_erls",Root_erls) (*FIXXXME:del with rls.rls'*)
15.10 ]);
15.11
15.12 @@ -252,7 +252,7 @@
15.13 ],
15.14 scr = Script ((term_of o the o (parse thy)) "empty_script")
15.15 }:rls);
15.16 -ruleset' := overwritelthy thy (!ruleset',
15.17 +ruleset' := overwritelthy @{theory} (!ruleset',
15.18 [("make_rooteq", make_rooteq)
15.19 ]);
15.20
15.21 @@ -326,7 +326,7 @@
15.22 }:rls);
15.23
15.24
15.25 -ruleset' := overwritelthy thy (!ruleset',
15.26 +ruleset' := overwritelthy @{theory} (!ruleset',
15.27 [("expand_rootbinoms", expand_rootbinoms)
15.28 ]);
15.29 *}
16.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Aug 31 16:00:13 2010 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Aug 31 16:38:22 2010 +0200
16.3 @@ -229,7 +229,7 @@
16.4 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "")
16.5 ];
16.6
16.7 -ruleset' := overwritelthy thy (!ruleset',
16.8 +ruleset' := overwritelthy @{theory} (!ruleset',
16.9 [("RootEq_erls",RootEq_erls),
16.10 (*FIXXXME:del with rls.rls'*)
16.11 ("rooteq_srls",rooteq_srls)
16.12 @@ -333,7 +333,7 @@
16.13 ],scr = Script ((term_of o the o (parse thy)) "empty_script")
16.14 }:rls);
16.15
16.16 -ruleset' := overwritelthy thy (!ruleset',
16.17 +ruleset' := overwritelthy @{theory} (!ruleset',
16.18 [("sqrt_isolate",sqrt_isolate)
16.19 ]);
16.20 (* -- left 28.08.02--*)
16.21 @@ -381,7 +381,7 @@
16.22 scr = Script ((term_of o the o (parse thy)) "empty_script")
16.23 }:rls);
16.24
16.25 -ruleset' := overwritelthy thy (!ruleset',
16.26 +ruleset' := overwritelthy @{theory} (!ruleset',
16.27 [("l_sqrt_isolate",l_sqrt_isolate)
16.28 ]);
16.29
16.30 @@ -430,7 +430,7 @@
16.31 scr = Script ((term_of o the o (parse thy)) "empty_script")
16.32 }:rls);
16.33
16.34 -ruleset' := overwritelthy thy (!ruleset',
16.35 +ruleset' := overwritelthy @{theory} (!ruleset',
16.36 [("r_sqrt_isolate",r_sqrt_isolate)
16.37 ]);
16.38
16.39 @@ -464,7 +464,7 @@
16.40 ],
16.41 scr = Script ((term_of o the o (parse thy)) "empty_script")
16.42 }:rls);
16.43 - ruleset' := overwritelthy thy (!ruleset',
16.44 + ruleset' := overwritelthy @{theory} (!ruleset',
16.45 [("rooteq_simplify",rooteq_simplify)
16.46 ]);
16.47
17.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Tue Aug 31 16:00:13 2010 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Tue Aug 31 16:38:22 2010 +0200
17.3 @@ -17,7 +17,7 @@
17.4 (append_rls "" e_rls
17.5 []));
17.6
17.7 -ruleset' := overwritelthy thy (!ruleset',
17.8 +ruleset' := overwritelthy @{theory} (!ruleset',
17.9 [("rootrat_erls",rootrat_erls) (*FIXXXME:del with rls.rls'*)]);
17.10
17.11 (*.calculate numeral groundterms.*)
17.12 @@ -31,7 +31,7 @@
17.13 (* "- z1 = -1 * z1" *)
17.14 Calc ("Root.sqrt",eval_sqrt "#sqrt_")
17.15 ];
17.16 -ruleset' := overwritelthy thy (!ruleset',
17.17 +ruleset' := overwritelthy @{theory} (!ruleset',
17.18 [("calculate_RootRat",calculate_RootRat)]);
17.19 *}
17.20
18.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Aug 31 16:00:13 2010 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Aug 31 16:38:22 2010 +0200
18.3 @@ -100,7 +100,7 @@
18.4 (append_rls "" e_rls
18.5 [])));
18.6
18.7 -ruleset' := overwritelthy thy (!ruleset',
18.8 +ruleset' := overwritelthy @{theory} (!ruleset',
18.9 [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);
18.10
18.11 (* Solves a rootrat Equation *)
18.12 @@ -121,7 +121,7 @@
18.13 ],
18.14 scr = Script ((term_of o the o (parse thy)) "empty_script")
18.15 }:rls);
18.16 -ruleset' := overwritelthy thy (!ruleset',
18.17 +ruleset' := overwritelthy @{theory} (!ruleset',
18.18 [("rootrat_solve",rootrat_solve)
18.19 ]);
18.20
19.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Tue Aug 31 16:00:13 2010 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Tue Aug 31 16:38:22 2010 +0200
19.3 @@ -1,12 +1,6 @@
19.4 (* simplification of terms
19.5 author: Walther Neuper 050912
19.6 (c) due to copyright terms
19.7 -
19.8 -remove_thy"Simplify";
19.9 -use_thy"~/proto2/isac/src/sml/Knowledge/Simplify";
19.10 -
19.11 -use_thy_only"~/proto2/isac/src/sml/Knowledge/Simplify";
19.12 -use_thy"~/proto2/isac/src/sml/Knowledge/Isac";
19.13 *)
19.14
19.15 theory Simplify imports Atools begin
19.16 @@ -14,7 +8,7 @@
19.17 consts
19.18
19.19 (*descriptions in the related problem*)
19.20 - term :: "real => una"
19.21 + TERM :: "real => una"
19.22 normalform :: "real => una"
19.23
19.24 (*the CAS-command*)
19.25 @@ -31,7 +25,7 @@
19.26 store_pbt
19.27 (prep_pbt (theory "Simplify") "pbl_simp" [] e_pblID
19.28 (["simplification"],
19.29 - [("#Given" ,["term t_"]),
19.30 + [("#Given" ,["TERM t_"]),
19.31 ("#Find" ,["normalform n_"])
19.32 ],
19.33 append_rls "e_rls" e_rls [(*for preds in where_*)],
19.34 @@ -41,7 +35,7 @@
19.35 store_pbt
19.36 (prep_pbt (theory "Simplify") "pbl_vereinfache" [] e_pblID
19.37 (["vereinfachen"],
19.38 - [("#Given" ,["term t_"]),
19.39 + [("#Given" ,["TERM t_"]),
19.40 ("#Find" ,["normalform n_"])
19.41 ],
19.42 append_rls "e_rls" e_rls [(*for preds in where_*)],
19.43 @@ -53,7 +47,7 @@
19.44 store_met
19.45 (prep_met (theory "Simplify") "met_simp" [] e_metID
19.46 (["simplification"],
19.47 - [("#Given" ,["term t_"]),
19.48 + [("#Given" ,["TERM t_"]),
19.49 ("#Find" ,["normalform n_"])
19.50 ],
19.51 {rew_ord'="tless_true",
19.52 @@ -74,7 +68,7 @@
19.53 "Simplify (2*a + 3*a)");
19.54 *)
19.55 fun argl2dtss t =
19.56 - [((term_of o the o (parse thy)) "term", t),
19.57 + [((term_of o the o (parse thy)) "TERM", t),
19.58 ((term_of o the o (parse thy)) "normalform",
19.59 [(term_of o the o (parse thy)) "N"])
19.60 ]
20.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Aug 31 16:00:13 2010 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Aug 31 16:38:22 2010 +0200
20.3 @@ -282,7 +282,7 @@
20.4 }:rls;
20.5
20.6
20.7 -ruleset' := overwritelthy thy (!ruleset',
20.8 +ruleset' := overwritelthy @{theory} (!ruleset',
20.9 [("testerls", prep_rls testerls)
20.10 ]);
20.11
20.12 @@ -495,7 +495,7 @@
20.13 eval_contains_root"#contains_root_"))
20.14 ];
20.15
20.16 -ruleset' := overwritelthy thy (!ruleset',
20.17 +ruleset' := overwritelthy @{theory} (!ruleset',
20.18 [("Test_simplify", prep_rls Test_simplify),
20.19 ("tval_rls", prep_rls tval_rls),
20.20 ("isolate_root", prep_rls isolate_root),
20.21 @@ -619,7 +619,7 @@
20.22
20.23
20.24
20.25 -ruleset' := overwritelthy thy (!ruleset',
20.26 +ruleset' := overwritelthy @{theory} (!ruleset',
20.27 [("norm_equation", prep_rls norm_equation),
20.28 ("ac_plus_times", prep_rls ac_plus_times),
20.29 ("rearrange_assoc", prep_rls rearrange_assoc)
20.30 @@ -1445,7 +1445,7 @@
20.31 }:rls;
20.32
20.33
20.34 -ruleset' := overwritelthy thy (!ruleset',
20.35 +ruleset' := overwritelthy @{theory} (!ruleset',
20.36 [("make_polytest", prep_rls make_polytest),
20.37 ("expand_binomtest", prep_rls expand_binomtest)
20.38 ]);
21.1 --- a/test/Tools/isac/Interpret/inform.sml Tue Aug 31 16:00:13 2010 +0200
21.2 +++ b/test/Tools/isac/Interpret/inform.sml Tue Aug 31 16:38:22 2010 +0200
21.3 @@ -471,7 +471,7 @@
21.4 "--------- inform [rational,simplification] ----------------------";
21.5 "--------- inform [rational,simplification] ----------------------";
21.6 states:=[];
21.7 -CalcTree [(["term (4/x - 3/y - 1)", "normalform N"],
21.8 +CalcTree [(["TERM (4/x - 3/y - 1)", "normalform N"],
21.9 ("Rational.thy",["rational","simplification"],
21.10 ["simplification","of_rationals"]))];
21.11 Iterator 1; moveActiveRoot 1;
22.1 --- a/test/Tools/isac/Interpret/rewtools.sml Tue Aug 31 16:00:13 2010 +0200
22.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Tue Aug 31 16:38:22 2010 +0200
22.3 @@ -464,14 +464,14 @@
22.4 "- because in assoc_thm'...";
22.5 val (thy, (thmid, ct')) = (Biegelinie.thy, ("sym_real_minus_eq_cancel",""));
22.6 val "s"::"y"::"m"::"_"::id = explode thmid;
22.7 -((num_str o (get_thm thy)) (implode id)) RS sym;
22.8 +((num_str @{o (get_thm thy)) (implode id)) RS sym;
22.9 ((get_thm thy) (implode id)) RS sym;
22.10 "... this creates [.]";
22.11 ((get_thm thy) (implode id));
22.12 "... while this has _NO_ [.]";
22.13
22.14 "----- thus we repair the [.] in string_of_thmI...";
22.15 -val thm = ((num_str o (get_thm thy)) (implode id)) RS sym;
22.16 +val thm = ((num_str @{o (get_thm thy)) (implode id)) RS sym;
22.17 if string_of_thmI thm = "(?b1 = ?a1) = (- ?b1 = - ?a1)" then ()
22.18 else raise error ("rewtools.sml: string_of_thmI " ^ string_of_thm thm ^
22.19 " = " ^ string_of_thmI thm);
22.20 @@ -520,7 +520,7 @@
22.21 "----------- fun is_contained_in ---------------------------------";
22.22 "----------- fun is_contained_in ---------------------------------";
22.23 "----------- fun is_contained_in ---------------------------------";
22.24 -val r1 = Thm ("real_diff_minus",num_str real_diff_minus);
22.25 +val r1 = Thm ("real_diff_minus",num_str @{real_diff_minus);
22.26 if contains_rule r1 Test_simplify then ()
22.27 else raise error "rewtools.sml contains_rule Thm";
22.28
23.1 --- a/test/Tools/isac/Interpret/solve.sml Tue Aug 31 16:00:13 2010 +0200
23.2 +++ b/test/Tools/isac/Interpret/solve.sml Tue Aug 31 16:38:22 2010 +0200
23.3 @@ -41,7 +41,7 @@
23.4 "--------- interSteps on norm_Rational ---------------------------";
23.5 "--------- interSteps on norm_Rational ---------------------------";
23.6 states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
23.7 -CalcTree [(["term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
23.8 +CalcTree [(["TERM ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
23.9 ("Rational.thy",
23.10 ["rational","simplification"],
23.11 ["simplification","of_rationals"]))];
24.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Tue Aug 31 16:00:13 2010 +0200
24.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Tue Aug 31 16:38:22 2010 +0200
24.3 @@ -145,9 +145,9 @@
24.4 Calc("op +", eval_binop "#add_")
24.5 ],
24.6 srls = Erls, calc = [],
24.7 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
24.8 + rules = [Thm ("nth_Cons_",num_str @{nth_Cons_),
24.9 Calc("op +", eval_binop "#add_"),
24.10 - Thm ("nth_Nil_",num_str nth_Nil_),
24.11 + Thm ("nth_Nil_",num_str @{nth_Nil_),
24.12 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
24.13 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
24.14 Calc("Atools.argument'_in",
24.15 @@ -1012,9 +1012,9 @@
24.16 val srls = append_rls "erls_IntegrierenUndK.." e_rls
24.17 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
24.18 Calc ("Atools.ident",eval_ident "#ident_"),
24.19 - Thm ("last_thmI",num_str last_thmI),
24.20 - Thm ("if_True",num_str if_True),
24.21 - Thm ("if_False",num_str if_False)
24.22 + Thm ("last_thmI",num_str @{last_thmI),
24.23 + Thm ("if_True",num_str @{if_True),
24.24 + Thm ("if_False",num_str @{if_False)
24.25 ]
24.26 ;
24.27 val t = str2term "last [1,2,3,4]";
25.1 --- a/test/Tools/isac/Knowledge/complex.sml Tue Aug 31 16:00:13 2010 +0200
25.2 +++ b/test/Tools/isac/Knowledge/complex.sml Tue Aug 31 16:38:22 2010 +0200
25.3 @@ -30,7 +30,7 @@
25.4 val SOME (t',_) =
25.5 rewrite_set_ thy false
25.6 (append_rls "simpl_complex" make_polynomial
25.7 - [Thm ("square_I", num_str square_I)]) t;
25.8 + [Thm ("square_I", num_str @{square_I)]) t;
25.9 term2str t';
25.10 "Float ((363, -2), 0, 0) + I__ * Float ((484, -2), 0, 0) +\
25.11 \I__ * Float ((726, -2), 0, 0) + -1 * Float ((968, -2), 0, 0)"
26.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Aug 31 16:00:13 2010 +0200
26.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Aug 31 16:38:22 2010 +0200
26.3 @@ -53,17 +53,17 @@
26.4 [("erls",
26.5 Rls {id = "erls",preconds = [], rew_ord = ("termlessI",termlessI),
26.6 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
26.7 - rules = [Thm ("refl",num_str refl),
26.8 - Thm ("le_refl",num_str le_refl),
26.9 - Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
26.10 - Thm ("not_true",num_str not_true),
26.11 - Thm ("not_false",num_str not_false),
26.12 + rules = [Thm ("refl",num_str @{refl),
26.13 + Thm ("real_le_refl",num_str @{thm real_le_refl}),
26.14 + Thm ("radd_left_cancel_le",num_str @{radd_left_cancel_le),
26.15 + Thm ("not_true",num_str @{not_true),
26.16 + Thm ("not_false",num_str @{not_false),
26.17 Thm ("and_true",and_true),
26.18 Thm ("and_false",and_false),
26.19 Thm ("or_true",or_true),
26.20 Thm ("or_false",or_false),
26.21 - Thm ("and_commute",num_str and_commute),
26.22 - Thm ("or_commute",num_str or_commute),
26.23 + Thm ("and_commute",num_str @{and_commute),
26.24 + Thm ("or_commute",num_str @{or_commute),
26.25
26.26 Calc ("Atools.is'_const",eval_const "#is_const_"),
26.27 Calc ("Atools.occurs'_in", eval_occurs_in ""),
26.28 @@ -270,7 +270,7 @@
26.29 val SOME (t'',_) = rewrite_set_ Isac.thy false make_polynomial t';
26.30 term2str t'';
26.31
26.32 - val thm = num_str realpow_eq_oneI;
26.33 + val thm = num_str @{realpow_eq_oneI;
26.34 case string_of_thm thm of
26.35
26.36
27.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue Aug 31 16:00:13 2010 +0200
27.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue Aug 31 16:38:22 2010 +0200
27.3 @@ -86,8 +86,8 @@
27.4 val t = str2term "length_ [x+y=1,y=2] = 2";
27.5 atomty t;
27.6 val testrls = append_rls "testrls" e_rls
27.7 - [(Thm ("length_Nil_",num_str length_Nil_)),
27.8 - (Thm ("length_Cons_",num_str length_Cons_)),
27.9 + [(Thm ("length_Nil_",num_str @{length_Nil_)),
27.10 + (Thm ("length_Cons_",num_str @{length_Cons_)),
27.11 Calc ("op +", eval_binop "#add_"),
27.12 Calc ("op =",eval_equal "#equal_")
27.13 ];
27.14 @@ -109,10 +109,10 @@
27.15 val SOME (t,_) =
27.16 rewrite_set_ thy true
27.17 (append_rls "prls_" e_rls
27.18 - [Thm ("nth_Cons_",num_str nth_Cons_),
27.19 - Thm ("nth_Nil_",num_str nth_Nil_),
27.20 - Thm ("tl_Cons",num_str tl_Cons),
27.21 - Thm ("tl_Nil",num_str tl_Nil),
27.22 + [Thm ("nth_Cons_",num_str @{nth_Cons_),
27.23 + Thm ("nth_Nil_",num_str @{nth_Nil_),
27.24 + Thm ("tl_Cons",num_str @{tl_Cons),
27.25 + Thm ("tl_Nil",num_str @{tl_Nil),
27.26 Calc ("EqSystem.occur'_exactly'_in",
27.27 eval_occur_exactly_in
27.28 "#eval_occur_exactly_in_")
27.29 @@ -1094,11 +1094,11 @@
27.30 \ 0 = c_4, \
27.31 \ 0 = c_3]";
27.32 val SOME (t,_) =
27.33 - rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
27.34 + rewrite_ thy e_rew_ord e_rls false (num_str @{commute_0_equality) t;
27.35 val SOME (t,_) =
27.36 - rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
27.37 + rewrite_ thy e_rew_ord e_rls false (num_str @{commute_0_equality) t;
27.38 val SOME (t,_) =
27.39 - rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
27.40 + rewrite_ thy e_rew_ord e_rls false (num_str @{commute_0_equality) t;
27.41 term2str t =
27.42 "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]";
27.43 val SOME (t,_) =
28.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue Aug 31 16:00:13 2010 +0200
28.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Aug 31 16:38:22 2010 +0200
28.3 @@ -60,7 +60,7 @@
28.4 rules = [(*for rewriting conditions in Thm's*)
28.5 Calc ("Atools.occurs'_in",
28.6 eval_occurs_in "#occurs_in_"),
28.7 - Thm ("not_true",num_str not_true),
28.8 + Thm ("not_true",num_str @{not_true),
28.9 Thm ("not_false",not_false)
28.10 ],
28.11 scr = EmptyScr};
28.12 @@ -146,8 +146,8 @@
28.13 rules = [Calc ("Tools.matches",eval_matches ""),
28.14 Calc ("Integrate.is'_f'_x",
28.15 eval_is_f_x "is_f_x_"),
28.16 - Thm ("not_true",num_str not_true),
28.17 - Thm ("not_false",num_str not_false)
28.18 + Thm ("not_true",num_str @{not_true),
28.19 + Thm ("not_false",num_str @{not_false)
28.20 ],
28.21 scr = EmptyScr};
28.22 fun rewrit thm t =
28.23 @@ -196,12 +196,12 @@
28.24 (*###*)val rls =
28.25 (append_rls "separate_bdv"
28.26 collect_bdv
28.27 - [Thm ("separate_bdv", num_str separate_bdv),
28.28 + [Thm ("separate_bdv", num_str @{separate_bdv),
28.29 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
28.30 - Thm ("separate_bdv_n", num_str separate_bdv_n),
28.31 - Thm ("separate_1_bdv", num_str separate_1_bdv),
28.32 + Thm ("separate_bdv_n", num_str @{separate_bdv_n),
28.33 + Thm ("separate_1_bdv", num_str @{separate_1_bdv),
28.34 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
28.35 - Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)
28.36 + Thm ("separate_1_bdv_n", num_str @{separate_1_bdv_n)
28.37 ]);
28.38 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
28.39 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
29.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue Aug 31 16:00:13 2010 +0200
29.2 +++ b/test/Tools/isac/Knowledge/poly.sml Tue Aug 31 16:38:22 2010 +0200
29.3 @@ -297,7 +297,7 @@
29.4 "-------- check pbl 'polynomial simplification' -----------------";
29.5 "-------- check pbl 'polynomial simplification' -----------------";
29.6 "-------- check pbl 'polynomial simplification' -----------------";
29.7 -val fmz = ["term ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
29.8 +val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
29.9 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
29.10 "normalform N"];
29.11 (*0*)
29.12 @@ -346,7 +346,7 @@
29.13 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
29.14 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
29.15 "-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
29.16 -val fmz = ["term ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
29.17 +val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
29.18 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
29.19 "normalform N"];
29.20 val (dI',pI',mI') =
29.21 @@ -374,7 +374,7 @@
29.22 "-------- interSteps for Schalk 299a -----------------------------";
29.23 states:=[];
29.24 CalcTree
29.25 -[(["term ((x - y)*(x + y))", "normalform N"],
29.26 +[(["TERM ((x - y)*(x + y))", "normalform N"],
29.27 ("Poly.thy",["polynomial","simplification"],
29.28 ["simplification","for_polynomials"]))];
29.29 Iterator 1;
30.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Tue Aug 31 16:00:13 2010 +0200
30.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Tue Aug 31 16:38:22 2010 +0200
30.3 @@ -250,7 +250,7 @@
30.4 "----------- pbl polynom vereinfachen p.33 -----------------------";
30.5 "----------- 140 c ---";
30.6 states:=[];
30.7 -CalcTree [(["term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
30.8 +CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
30.9 "normalform N"],
30.10 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
30.11 ["simplification","for_polynomials","with_minus"]))];
30.12 @@ -263,7 +263,7 @@
30.13
30.14 "----------- 140 d ---";
30.15 states:=[];
30.16 -CalcTree [(["term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
30.17 +CalcTree [(["TERM (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
30.18 "normalform N"],
30.19 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
30.20 ["simplification","for_polynomials","with_minus"]))];
30.21 @@ -277,7 +277,7 @@
30.22
30.23 "----------- 139 c ---";
30.24 states:=[];
30.25 -CalcTree [(["term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
30.26 +CalcTree [(["TERM (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
30.27 "normalform N"],
30.28 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
30.29 ["simplification","for_polynomials","with_minus"]))];
30.30 @@ -290,7 +290,7 @@
30.31
30.32 "----------- 139 b ---";
30.33 states:=[];
30.34 -CalcTree [(["term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
30.35 +CalcTree [(["TERM (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
30.36 "normalform N"],
30.37 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
30.38 ["simplification","for_polynomials","with_minus"]))];
30.39 @@ -303,7 +303,7 @@
30.40
30.41 "----------- 138 a ---";
30.42 states:=[];
30.43 -CalcTree [(["term (2*u - 3*v - 6*u + 5*v)",
30.44 +CalcTree [(["TERM (2*u - 3*v - 6*u + 5*v)",
30.45 "normalform N"],
30.46 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
30.47 ["simplification","for_polynomials","with_minus"]))];
30.48 @@ -357,7 +357,7 @@
30.49 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
30.50 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
30.51 states:=[];
30.52 -CalcTree [(["term (2*u - 5 - (3 - 4*u) + (8*u + 9))",
30.53 +CalcTree [(["TERM (2*u - 5 - (3 - 4*u) + (8*u + 9))",
30.54 "normalform N"],
30.55 ("PolyMinus.thy",["klammer","polynom","vereinfachen"],
30.56 ["simplification","for_polynomials","with_parentheses"]))];
30.57 @@ -388,7 +388,7 @@
30.58 "----------- try fun applyTactics --------------------------------";
30.59 "----------- try fun applyTactics --------------------------------";
30.60 states:=[];
30.61 -CalcTree [(["term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
30.62 +CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
30.63 "normalform N"],
30.64 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
30.65 ["simplification","for_polynomials","with_minus"]))];
30.66 @@ -448,7 +448,7 @@
30.67 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
30.68
30.69 states:=[];
30.70 -CalcTree [(["term (- (8 * g) + 10 * g + h)",
30.71 +CalcTree [(["TERM (- (8 * g) + 10 * g + h)",
30.72 "normalform N"],
30.73 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
30.74 ["simplification","for_polynomials","with_minus"]))];
30.75 @@ -460,7 +460,7 @@
30.76
30.77
30.78 states:=[];
30.79 -CalcTree [(["term (- (8 * g) + 10 * g + f)",
30.80 +CalcTree [(["TERM (- (8 * g) + 10 * g + f)",
30.81 "normalform N"],
30.82 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"],
30.83 ["simplification","for_polynomials","with_minus"]))];
30.84 @@ -509,7 +509,7 @@
30.85
30.86 (*@@@@@@@*)
30.87 states:=[];
30.88 -CalcTree [(["term ((3*a + 2) * (4*a - 1))",
30.89 +CalcTree [(["TERM ((3*a + 2) * (4*a - 1))",
30.90 "normalform N"],
30.91 ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"],
30.92 ["simplification","for_polynomials","with_parentheses_mult"]))];
30.93 @@ -528,7 +528,7 @@
30.94 "----------- pbl binom polynom vereinfachen: cube ----------------";
30.95 "----------- pbl binom polynom vereinfachen: cube ----------------";
30.96 states:=[];
30.97 -CalcTree [(["term (8*(a - q) + a - 2*q + 3*(a - 2*q))",
30.98 +CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))",
30.99 "normalform N"],
30.100 ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"],
30.101 ["simplification","for_polynomials","with_parentheses_mult"]))];
30.102 @@ -540,7 +540,7 @@
30.103 "----------- refine Vereinfache ----------------------------------";
30.104 "----------- refine Vereinfache ----------------------------------";
30.105 "----------- refine Vereinfache ----------------------------------";
30.106 -val fmz = ["term (8*(a - q) + a - 2*q + 3*(a - 2*q))",
30.107 +val fmz = ["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))",
30.108 "normalform N"];
30.109 print_depth 11;
30.110 val matches = refine fmz ["vereinfachen"];
30.111 @@ -565,9 +565,9 @@
30.112 (*"(?a | True) = True"*)
30.113 Thm ("or_false",or_false),
30.114 (*"(?a | False) = ?a"*)
30.115 - Thm ("not_true",num_str not_true),
30.116 + Thm ("not_true",num_str @{not_true),
30.117 (*"(~ True) = False"*)
30.118 - Thm ("not_false",num_str not_false)
30.119 + Thm ("not_false",num_str @{not_false)
30.120 (*"(~ False) = True"*)];
30.121 trace_rewrite := true;
30.122 val SOME (t', _) = rewrite_set_ thy false prls t;
31.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Aug 31 16:00:13 2010 +0200
31.2 +++ b/test/Tools/isac/Knowledge/rational.sml Tue Aug 31 16:38:22 2010 +0200
31.3 @@ -983,7 +983,7 @@
31.4 "True";
31.5 val t = str2term "(6*x)^^^2";
31.6 val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false
31.7 - (num_str realpow_def_atom) t;
31.8 + (num_str @{realpow_def_atom) t;
31.9 term2str t';
31.10 trace_rewrite:=false;
31.11
31.12 @@ -1824,7 +1824,7 @@
31.13 "-------- me Schalk I No.186 -------------------------------------";
31.14 "-------- me Schalk I No.186 -------------------------------------";
31.15 "-------- me Schalk I No.186 -------------------------------------";
31.16 -val fmz = ["term ((14 * x * y) / ( x * y ))",
31.17 +val fmz = ["TERM ((14 * x * y) / ( x * y ))",
31.18 "normalform N"];
31.19 val (dI',pI',mI') =
31.20 ("Rational.thy",["rational","simplification"],
31.21 @@ -1852,7 +1852,7 @@
31.22 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
31.23 states:=[];
31.24 CalcTree
31.25 -[(["term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
31.26 +[(["TERM (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
31.27 ("Rational.thy",["rational","simplification"],
31.28 ["simplification","of_rationals"]))];
31.29 Iterator 1;
31.30 @@ -1869,7 +1869,7 @@
31.31 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
31.32 states:=[];
31.33 CalcTree
31.34 -[(["term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
31.35 +[(["TERM ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
31.36 ("Rational.thy",["rational","simplification"],
31.37 ["simplification","of_rationals"]))];
31.38 Iterator 1;
32.1 --- a/test/Tools/isac/Knowledge/simplify.sml Tue Aug 31 16:00:13 2010 +0200
32.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Tue Aug 31 16:38:22 2010 +0200
32.3 @@ -40,7 +40,7 @@
32.4 "----------- append inform with final result ---------------------";
32.5 "----------- append inform with final result ---------------------";
32.6 states:=[];
32.7 -CalcTree [(["term ((14 * x * y) / ( x * y ))", "normalform N"],
32.8 +CalcTree [(["TERM ((14 * x * y) / ( x * y ))", "normalform N"],
32.9 ("Rational.thy",["rational","simplification"],
32.10 ["simplification","of_rationals"]))];
32.11 Iterator 1;
33.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Tue Aug 31 16:00:13 2010 +0200
33.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Aug 31 16:38:22 2010 +0200
33.3 @@ -143,7 +143,7 @@
33.4 " _________________ rewrite_ x+4_________________ ";
33.5 " _________________ rewrite_ x+4_________________ ";
33.6 val t = (term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
33.7 -val thm = num_str square_equation_left;
33.8 +val thm = num_str @{square_equation_left;
33.9 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
33.10 val rls = Test_simplify;
33.11 val (t,_) = the (rewrite_set_ thy false rls t);
33.12 @@ -187,7 +187,7 @@
33.13
33.14 28.8.02: ruleset besser zusammenstellen !!!
33.15 *)
33.16 -val thm = num_str square_equation_left;
33.17 +val thm = num_str @{square_equation_left;
33.18 val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);
33.19 val asm = asm union asm';
33.20 val rls = Test_simplify;
33.21 @@ -209,7 +209,7 @@
33.22 " _________________ rewrite x=4_________________ ";
33.23 " _________________ rewrite x=4_________________ ";
33.24 (*
33.25 -rewrite thy' "tless_true" "tval_rls" true (num_str rbinom_power_2) ct;
33.26 +rewrite thy' "tless_true" "tval_rls" true (num_str @{rbinom_power_2) ct;
33.27 atomty ((#prop o rep_thm) (!tthm));
33.28 atomty (term_of (!tct));
33.29 *)
34.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Aug 31 16:00:13 2010 +0200
34.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Tue Aug 31 16:38:22 2010 +0200
34.3 @@ -330,7 +330,7 @@
34.4 *** Const ( HOL.divide, [real, real] => real)
34.5 *** . Free ( aaa, real)
34.6 *** . Free ( 1, real) *)
34.7 - val thm = num_str real_divide_1;
34.8 + val thm = num_str @{thm divide_1};
34.9 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
34.10 (*val t = Free ("aaa","RealDef.real") : term*)
34.11
34.12 @@ -365,7 +365,7 @@
34.13 *** Const ( Nat.power, [real, nat] => real)
34.14 *** . Free ( 1, real)
34.15 *** . Free ( aaa, nat) .......................... nat !!! *)
34.16 - val thm = num_str realpow_eq_one;
34.17 + val thm = num_str @{realpow_eq_one;
34.18 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
34.19 (*val t = Free ("1","RealDef.real") : term*)
34.20
35.1 --- a/test/Tools/isac/ProgLang/listg.sml Tue Aug 31 16:00:13 2010 +0200
35.2 +++ b/test/Tools/isac/ProgLang/listg.sml Tue Aug 31 16:38:22 2010 +0200
35.3 @@ -14,7 +14,7 @@
35.4 atomty t;
35.5 val thm = (#prop o rep_thm o num_str) nth_Cons_;
35.6 atomty thm;
35.7 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Cons_) t;
35.8 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{nth_Cons_) t;
35.9 if term2str t' = "nth_ (3 + - 1) [b, c, d, e]" then ()
35.10 else raise error "list_rls.sml, nth_ (3 + - 1) [b, c, d, e]";
35.11
35.12 @@ -22,7 +22,7 @@
35.13 atomty t;
35.14 val thm = (#prop o rep_thm o num_str) nth_Nil_;
35.15 atomty thm;
35.16 -val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str nth_Nil_) t;
35.17 +val SOME (t',_) = rewrite_ thy dummy_ord Poly_erls false (num_str @{nth_Nil_) t;
35.18 term2str t';
35.19 "a";
35.20
36.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Tue Aug 31 16:00:13 2010 +0200
36.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Tue Aug 31 16:38:22 2010 +0200
36.3 @@ -192,7 +192,7 @@
36.4 eval_occur_exactly_in
36.5 "#eval_occur_exactly_in_"))
36.6 ])
36.7 - false bdvs (num_str separate_bdvs_add) t;
36.8 + false bdvs (num_str @{separate_bdvs_add) t;
36.9 (writeln o term2str) t;
36.10 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
36.11 then () else raise error "rewrite.sml rewrite_inst_ bdvs";
37.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Tue Aug 31 16:00:13 2010 +0200
37.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Tue Aug 31 16:38:22 2010 +0200
37.3 @@ -28,7 +28,7 @@
37.4 store_met
37.5 (prep_met Test.thy "met_testinter" [] e_metID
37.6 (["Test","test_interSteps_1"]:metID,
37.7 - [("#Given" ,["term t_"]),
37.8 + [("#Given" ,["TERM t_"]),
37.9 ("#Find" ,["normalform n_"])
37.10 ],
37.11 {rew_ord'="dummy_ord",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
37.12 @@ -58,7 +58,7 @@
37.13 (*the structure of the auto-gen. script is interpreted correctly*)
37.14 states:=[];
37.15 CalcTree
37.16 -[(["term (b + a - b)",(*this is Schalk 299b*)
37.17 +[(["TERM (b + a - b)",(*this is Schalk 299b*)
37.18 "normalform N"],
37.19 ("Poly.thy",["polynomial","simplification"],
37.20 ["Test","test_interSteps_1"]))];
37.21 @@ -95,7 +95,7 @@
37.22
37.23 states:=[];
37.24 CalcTree
37.25 -[(["term (b + a - b)", "normalform N"],
37.26 +[(["TERM (b + a - b)", "normalform N"],
37.27 ("Poly.thy",["polynomial","simplification"],
37.28 ["simplification","for_polynomials"]))];
37.29 Iterator 1;
37.30 @@ -154,7 +154,7 @@
37.31 ***)
37.32 states:=[];
37.33 CalcTree
37.34 -[(["term (b + a - b)", "normalform N"],
37.35 +[(["TERM (b + a - b)", "normalform N"],
37.36 ("Poly.thy",["polynomial","simplification"],
37.37 ["simplification","of_rationals"]))];
37.38 Iterator 1;
38.1 --- a/test/Tools/isac/ProgLang/term_G.sml Tue Aug 31 16:00:13 2010 +0200
38.2 +++ b/test/Tools/isac/ProgLang/term_G.sml Tue Aug 31 16:38:22 2010 +0200
38.3 @@ -23,16 +23,16 @@
38.4 "----------- inst_bdv --------------------------------------------";
38.5 "----------- inst_bdv --------------------------------------------";
38.6 "----------- inst_bdv --------------------------------------------";
38.7 -if string_of_thm (num_str d1_isolate_add2) =
38.8 +if string_of_thm (num_str @{d1_isolate_add2) =
38.9 "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
38.10 else raise error "term_G.sml d1_isolate_add2";
38.11 val subst = [(str2term "bdv", str2term "x")];
38.12 -val t = (norm o #prop o rep_thm) (num_str d1_isolate_add2);
38.13 +val t = (norm o #prop o rep_thm) (num_str @{d1_isolate_add2);
38.14 val t' = inst_bdv subst t;
38.15 if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
38.16 else raise error "term_G.sml inst_bdv 1";
38.17
38.18 -if string_of_thm (num_str separate_bdvs_add) =
38.19 +if string_of_thm (num_str @{separate_bdvs_add) =
38.20 "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
38.21 \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
38.22 else raise error "term_G.sml separate_bdvs_add";
38.23 @@ -40,7 +40,7 @@
38.24 (str2term"bdv_2",str2term"c_2"),
38.25 (str2term"bdv_3",str2term"c_3"),
38.26 (str2term"bdv_4",str2term"c_4")];
38.27 -val t = (norm o #prop o rep_thm) (num_str separate_bdvs_add);
38.28 +val t = (norm o #prop o rep_thm) (num_str @{separate_bdvs_add);
38.29 val t' = inst_bdv subst t;
38.30 if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
38.31 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
39.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Tue Aug 31 16:00:13 2010 +0200
39.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Tue Aug 31 16:38:22 2010 +0200
39.3 @@ -212,12 +212,12 @@
39.4
39.5 val it = () : unit
39.6 *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
39.7 -*** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
39.8 +*** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]
39.9 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"]
39.10 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"]
39.11 *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
39.12 *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"]
39.13 -*** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
39.14 +*** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]
39.15 *** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"]
39.16 *** insert: preserved ["IsacScripts","ListG","Theorems","induct"]
39.17 *** insert: preserved ["IsacScripts","ListG","Theorems","simps_1"]
39.18 @@ -233,8 +233,8 @@
39.19 ----------------------------------
39.20
39.21 val it = () : unit
39.22 -*** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]
39.23 -*** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]*)
39.24 +*** insert: not found ["Isabelle","NatDef","Theorems","real_le_refl"]
39.25 +*** insert: not found ["Isabelle","NatDef","Theorems","real_le_refl"]*)
39.26
39.27 "----------- ### thes2file ... Exception- Match raised -----------";
39.28 "----------- ### thes2file ... Exception- Match raised -----------";