1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Wed Sep 01 16:15:13 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Wed Sep 01 16:43:58 2010 +0200
1.3 @@ -22,15 +22,17 @@
1.4 ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9)
1.5
1.6 ML {*
1.7 +val thy = @{theory};
1.8 +
1.9 (** problems **)
1.10
1.11 store_pbt
1.12 - (prep_pbt (theory "AlgEin") "pbl_algein" [] e_pblID
1.13 + (prep_pbt thy "pbl_algein" [] e_pblID
1.14 (["Berechnung"], [], e_rls, NONE,
1.15 []));
1.16 (* WN070405
1.17 store_pbt
1.18 - (prep_pbt (theory "AlgEin") "pbl_algein_num" [] e_pblID
1.19 + (prep_pbt thy "pbl_algein_num" [] e_pblID
1.20 (["numerische", "Berechnung"],
1.21 [("#Given" ,["KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),
1.22 ("#Find" ,["GesamtLaenge l_"])
1.23 @@ -40,7 +42,7 @@
1.24 []));
1.25 *)
1.26 store_pbt
1.27 - (prep_pbt (theory "AlgEin") "pbl_algein_numsym" [] e_pblID
1.28 + (prep_pbt thy "pbl_algein_numsym" [] e_pblID
1.29 (["numerischSymbolische", "Berechnung"],
1.30 [("#Given" ,["KantenLaenge k_","Querschnitt q__"(*q_ in Biegelinie.thy*),
1.31 "KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),
1.32 @@ -57,7 +59,7 @@
1.33 (** methods **)
1.34
1.35 store_met
1.36 - (prep_met (theory "AlgEin") "met_algein" [] e_metID
1.37 + (prep_met thy "met_algein" [] e_metID
1.38 (["Berechnung"],
1.39 [],
1.40 {rew_ord'="tless_true", rls'= Erls, calc = [],
1.41 @@ -67,7 +69,7 @@
1.42 ));
1.43
1.44 store_met
1.45 - (prep_met (theory "AlgEin") "met_algein_numsym" [] e_metID
1.46 + (prep_met thy "met_algein_numsym" [] e_metID
1.47 (["Berechnung","erstNumerisch"],
1.48 [],
1.49 {rew_ord'="tless_true", rls'= Erls, calc = [],
1.50 @@ -77,7 +79,7 @@
1.51 ));
1.52
1.53 store_met
1.54 - (prep_met (theory "AlgEin") "met_algein_numsym" [] e_metID
1.55 + (prep_met thy "met_algein_numsym" [] e_metID
1.56 (["Berechnung","erstNumerisch"],
1.57 [("#Given" ,["KantenLaenge k_","Querschnitt q__",
1.58 "KantenUnten u_", "KantenSenkrecht s_",
1.59 @@ -111,7 +113,7 @@
1.60 ));
1.61
1.62 store_met
1.63 - (prep_met (theory "AlgEin") "met_algein_symnum" [] e_metID
1.64 + (prep_met thy "met_algein_symnum" [] e_metID
1.65 (["Berechnung","erstSymbolisch"],
1.66 [("#Given" ,["KantenLaenge k_","Querschnitt q__",
1.67 "KantenUnten u_", "KantenSenkrecht s_",
2.1 --- a/src/Tools/isac/Knowledge/Atools.thy Wed Sep 01 16:15:13 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Wed Sep 01 16:43:58 2010 +0200
2.3 @@ -130,6 +130,7 @@
2.4 *}
2.5
2.6 ML {*
2.7 +val thy = @{theory};
2.8
2.9 (** evaluation of numerals and special predicates on the meta-level **)
2.10 (*-------------------------functions---------------------*)
2.11 @@ -557,7 +558,7 @@
2.12 Thm ("if_False",num_str @{thm if_False})
2.13 ];
2.14
2.15 -ruleset' := overwritelthy @{theory} (!ruleset',
2.16 +ruleset' := overwritelthy thy (!ruleset',
2.17 [("list_rls",list_rls)
2.18 ]);
2.19
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Sep 01 16:15:13 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Sep 01 16:43:58 2010 +0200
3.3 @@ -72,33 +72,35 @@
3.4 make_fun_explicit "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
3.5
3.6 ML {*
3.7 +val thy = @{theory};
3.8 +
3.9 (** theory elements for transfer into html **)
3.10
3.11 store_isa ["IsacKnowledge"] [];
3.12 -store_thy (theory "Biegelinie")
3.13 +store_thy thy
3.14 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
3.15 -store_isa ["IsacKnowledge", theory2thyID (theory "Biegelinie"), "Theorems"]
3.16 +store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"]
3.17 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
3.18 -store_thm (theory "Biegelinie") ("Belastung_Querkraft", Belastung_Querkraft)
3.19 +store_thm thy ("Belastung_Querkraft", Belastung_Querkraft)
3.20 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
3.21 -store_thm (theory "Biegelinie") ("Moment_Neigung", Moment_Neigung)
3.22 +store_thm thy ("Moment_Neigung", Moment_Neigung)
3.23 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
3.24 -store_thm (theory "Biegelinie") ("Moment_Querkraft", Moment_Querkraft)
3.25 +store_thm thy ("Moment_Querkraft", Moment_Querkraft)
3.26 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
3.27 -store_thm (theory "Biegelinie") ("Neigung_Moment", Neigung_Moment)
3.28 +store_thm thy ("Neigung_Moment", Neigung_Moment)
3.29 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
3.30 -store_thm (theory "Biegelinie") ("Querkraft_Belastung", Querkraft_Belastung)
3.31 +store_thm thy ("Querkraft_Belastung", Querkraft_Belastung)
3.32 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
3.33 -store_thm (theory "Biegelinie") ("Querkraft_Moment", Querkraft_Moment)
3.34 +store_thm thy ("Querkraft_Moment", Querkraft_Moment)
3.35 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
3.36 -store_thm (theory "Biegelinie") ("make_fun_explicit", make_fun_explicit)
3.37 +store_thm thy ("make_fun_explicit", make_fun_explicit)
3.38 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
3.39
3.40
3.41 (** problems **)
3.42
3.43 store_pbt
3.44 - (prep_pbt (theory "Biegelinie") "pbl_bieg" [] e_pblID
3.45 + (prep_pbt thy "pbl_bieg" [] e_pblID
3.46 (["Biegelinien"],
3.47 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
3.48 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
3.49 @@ -110,7 +112,7 @@
3.50 [["IntegrierenUndKonstanteBestimmen2"]]));
3.51
3.52 store_pbt
3.53 - (prep_pbt (theory "Biegelinie") "pbl_bieg_mom" [] e_pblID
3.54 + (prep_pbt thy "pbl_bieg_mom" [] e_pblID
3.55 (["MomentBestimmte","Biegelinien"],
3.56 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
3.57 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
3.58 @@ -122,7 +124,7 @@
3.59 [["IntegrierenUndKonstanteBestimmen"]]));
3.60
3.61 store_pbt
3.62 - (prep_pbt (theory "Biegelinie") "pbl_bieg_momg" [] e_pblID
3.63 + (prep_pbt thy "pbl_bieg_momg" [] e_pblID
3.64 (["MomentGegebene","Biegelinien"],
3.65 [],
3.66 append_rls "e_rls" e_rls [],
3.67 @@ -130,7 +132,7 @@
3.68 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]]));
3.69
3.70 store_pbt
3.71 - (prep_pbt (theory "Biegelinie") "pbl_bieg_einf" [] e_pblID
3.72 + (prep_pbt thy "pbl_bieg_einf" [] e_pblID
3.73 (["einfache","Biegelinien"],
3.74 [],
3.75 append_rls "e_rls" e_rls [],
3.76 @@ -138,7 +140,7 @@
3.77 [["IntegrierenUndKonstanteBestimmen","4x4System"]]));
3.78
3.79 store_pbt
3.80 - (prep_pbt (theory "Biegelinie") "pbl_bieg_momquer" [] e_pblID
3.81 + (prep_pbt thy "pbl_bieg_momquer" [] e_pblID
3.82 (["QuerkraftUndMomentBestimmte","Biegelinien"],
3.83 [],
3.84 append_rls "e_rls" e_rls [],
3.85 @@ -146,7 +148,7 @@
3.86 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]]));
3.87
3.88 store_pbt
3.89 - (prep_pbt (theory "Biegelinie") "pbl_bieg_vonq" [] e_pblID
3.90 + (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
3.91 (["vonBelastungZu","Biegelinien"],
3.92 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
3.93 ("#Find" ,["Funktionen funs___"])],
3.94 @@ -155,7 +157,7 @@
3.95 [["Biegelinien","ausBelastung"]]));
3.96
3.97 store_pbt
3.98 - (prep_pbt (theory "Biegelinie") "pbl_bieg_randbed" [] e_pblID
3.99 + (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
3.100 (["setzeRandbedingungen","Biegelinien"],
3.101 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
3.102 ("#Find" ,["Gleichungen equs___"])],
3.103 @@ -164,7 +166,7 @@
3.104 [["Biegelinien","setzeRandbedingungenEin"]]));
3.105
3.106 store_pbt
3.107 - (prep_pbt (theory "Biegelinie") "pbl_equ_fromfun" [] e_pblID
3.108 + (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
3.109 (["makeFunctionTo","equation"],
3.110 [("#Given" ,["functionEq fun_","substitution sub_"]),
3.111 ("#Find" ,["equality equ___"])],
3.112 @@ -223,7 +225,7 @@
3.113 scr = EmptyScr};
3.114
3.115 store_met
3.116 - (prep_met (theory "Biegelinie") "met_biege" [] e_metID
3.117 + (prep_met thy "met_biege" [] e_metID
3.118 (["IntegrierenUndKonstanteBestimmen"],
3.119 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
3.120 "FunktionsVariable v_"]),
3.121 @@ -301,7 +303,7 @@
3.122 ));
3.123
3.124 store_met
3.125 - (prep_met (theory "Biegelinie") "met_biege_2" [] e_metID
3.126 + (prep_met thy "met_biege_2" [] e_metID
3.127 (["IntegrierenUndKonstanteBestimmen2"],
3.128 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
3.129 "FunktionsVariable v_"]),
3.130 @@ -344,7 +346,7 @@
3.131 ));
3.132
3.133 store_met
3.134 - (prep_met (theory "Biegelinie") "met_biege_intconst_2" [] e_metID
3.135 + (prep_met thy "met_biege_intconst_2" [] e_metID
3.136 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
3.137 [],
3.138 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.139 @@ -355,7 +357,7 @@
3.140 ));
3.141
3.142 store_met
3.143 - (prep_met (theory "Biegelinie") "met_biege_intconst_4" [] e_metID
3.144 + (prep_met thy "met_biege_intconst_4" [] e_metID
3.145 (["IntegrierenUndKonstanteBestimmen","4x4System"],
3.146 [],
3.147 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.148 @@ -366,7 +368,7 @@
3.149 ));
3.150
3.151 store_met
3.152 - (prep_met (theory "Biegelinie") "met_biege_intconst_1" [] e_metID
3.153 + (prep_met thy "met_biege_intconst_1" [] e_metID
3.154 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
3.155 [],
3.156 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.157 @@ -377,7 +379,7 @@
3.158 ));
3.159
3.160 store_met
3.161 - (prep_met (theory "Biegelinie") "met_biege2" [] e_metID
3.162 + (prep_met thy "met_biege2" [] e_metID
3.163 (["Biegelinien"],
3.164 [],
3.165 {rew_ord'="tless_true", rls'=Erls, calc = [],
3.166 @@ -388,7 +390,7 @@
3.167 ));
3.168
3.169 store_met
3.170 - (prep_met (theory "Biegelinie") "met_biege_ausbelast" [] e_metID
3.171 + (prep_met thy "met_biege_ausbelast" [] e_metID
3.172 (["Biegelinien","ausBelastung"],
3.173 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
3.174 ("#Find" ,["Funktionen funs_"])],
3.175 @@ -428,7 +430,7 @@
3.176 ));
3.177
3.178 store_met
3.179 - (prep_met (theory "Biegelinie") "met_biege_setzrand" [] e_metID
3.180 + (prep_met thy "met_biege_setzrand" [] e_metID
3.181 (["Biegelinien","setzeRandbedingungenEin"],
3.182 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
3.183 ("#Find" ,["Gleichungen equs___"])],
3.184 @@ -492,7 +494,7 @@
3.185 ));
3.186
3.187 store_met
3.188 - (prep_met (theory "Biegelinie") "met_equ_fromfun" [] e_metID
3.189 + (prep_met thy "met_equ_fromfun" [] e_metID
3.190 (["Equation","fromFunction"],
3.191 [("#Given" ,["functionEq fun_","substitution sub_"]),
3.192 ("#Find" ,["equality equ___"])],
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Sep 01 16:15:13 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Sep 01 16:43:58 2010 +0200
4.3 @@ -90,6 +90,8 @@
4.4 realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
4.5
4.6 ML {*
4.7 +val thy = @{theory};
4.8 +
4.9 (** eval functions **)
4.10
4.11 fun primed (Const (id, T)) = Const (id ^ "'", T)
4.12 @@ -239,11 +241,11 @@
4.13 (** problem types **)
4.14
4.15 store_pbt
4.16 - (prep_pbt (theory "Diff") "pbl_fun" [] e_pblID
4.17 + (prep_pbt thy "pbl_fun" [] e_pblID
4.18 (["function"], [], e_rls, NONE, []));
4.19
4.20 store_pbt
4.21 - (prep_pbt (theory "Diff") "pbl_fun_deriv" [] e_pblID
4.22 + (prep_pbt thy "pbl_fun_deriv" [] e_pblID
4.23 (["derivative_of","function"],
4.24 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
4.25 ("#Find" ,["derivative f_'_"])
4.26 @@ -254,7 +256,7 @@
4.27
4.28 (*here "named" is used differently from Integration"*)
4.29 store_pbt
4.30 - (prep_pbt (theory "Diff") "pbl_fun_deriv_nam" [] e_pblID
4.31 + (prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID
4.32 (["named","derivative_of","function"],
4.33 [("#Given" ,["functionEq f_","differentiateFor v_"]),
4.34 ("#Find" ,["derivativeEq f_'_"])
4.35 @@ -266,13 +268,13 @@
4.36 (** methods **)
4.37
4.38 store_met
4.39 - (prep_met (theory "Diff") "met_diff" [] e_metID
4.40 + (prep_met thy "met_diff" [] e_metID
4.41 (["diff"], [],
4.42 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
4.43 crls = Atools_erls, nrls = norm_diff}, "empty_script"));
4.44
4.45 store_met
4.46 - (prep_met (theory "Diff") "met_diff_onR" [] e_metID
4.47 + (prep_met thy "met_diff_onR" [] e_metID
4.48 (["diff","differentiate_on_R"],
4.49 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
4.50 ("#Find" ,["derivative f_'_"])
4.51 @@ -304,7 +306,7 @@
4.52 ));
4.53
4.54 store_met
4.55 - (prep_met (theory "Diff") "met_diff_simpl" [] e_metID
4.56 + (prep_met thy "met_diff_simpl" [] e_metID
4.57 (["diff","diff_simpl"],
4.58 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
4.59 ("#Find" ,["derivative f_'_"])
4.60 @@ -336,7 +338,7 @@
4.61 ));
4.62
4.63 store_met
4.64 - (prep_met (theory "Diff") "met_diff_equ" [] e_metID
4.65 + (prep_met thy "met_diff_equ" [] e_metID
4.66 (["diff","differentiate_equality"],
4.67 [("#Given" ,["functionEq f_","differentiateFor v_"]),
4.68 ("#Find" ,["derivativeEq f_'_"])
4.69 @@ -369,7 +371,7 @@
4.70 ));
4.71
4.72 store_met
4.73 - (prep_met (theory "Diff") "met_diff_after_simp" [] e_metID
4.74 + (prep_met thy "met_diff_after_simp" [] e_metID
4.75 (["diff","after_simplification"],
4.76 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
4.77 ("#Find" ,["derivative f_'_"])
5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 01 16:15:13 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 01 16:43:58 2010 +0200
5.3 @@ -48,6 +48,8 @@
5.4 *}
5.5
5.6 ML {*
5.7 +val thy = @{theory};
5.8 +
5.9 val eval_rls = prep_rls(
5.10 Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),
5.11 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
5.12 @@ -83,7 +85,7 @@
5.13 (** problem types **)
5.14
5.15 store_pbt
5.16 - (prep_pbt (theory "DiffApp") "pbl_fun_max" [] e_pblID
5.17 + (prep_pbt thy "pbl_fun_max" [] e_pblID
5.18 (["maximum_of","function"],
5.19 [("#Given" ,["fixedValues fix_"]),
5.20 ("#Find" ,["maximum m_","valuesFor vs_"]),
5.21 @@ -92,21 +94,21 @@
5.22 e_rls, NONE, []));
5.23
5.24 store_pbt
5.25 - (prep_pbt (theory "DiffApp") "pbl_fun_make" [] e_pblID
5.26 + (prep_pbt thy "pbl_fun_make" [] e_pblID
5.27 (["make","function"]:pblID,
5.28 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
5.29 ("#Find" ,["functionEq f_1_"])
5.30 ],
5.31 e_rls, NONE, []));
5.32 store_pbt
5.33 - (prep_pbt (theory "DiffApp") "pbl_fun_max_expl" [] e_pblID
5.34 + (prep_pbt thy "pbl_fun_max_expl" [] e_pblID
5.35 (["by_explicit","make","function"]:pblID,
5.36 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
5.37 ("#Find" ,["functionEq f_1_"])
5.38 ],
5.39 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]]));
5.40 store_pbt
5.41 - (prep_pbt (theory "DiffApp") "pbl_fun_max_newvar" [] e_pblID
5.42 + (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID
5.43 (["by_new_variable","make","function"]:pblID,
5.44 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
5.45 (*WN.12.5.03: precond for distinction still missing*)
5.46 @@ -115,7 +117,7 @@
5.47 e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]]));
5.48
5.49 store_pbt
5.50 - (prep_pbt (theory "DiffApp") "pbl_fun_max_interv" [] e_pblID
5.51 + (prep_pbt thy "pbl_fun_max_interv" [] e_pblID
5.52 (["on_interval","maximum_of","function"]:pblID,
5.53 [("#Given" ,["functionEq t_","boundVariable v_","interval itv_"]),
5.54 (*WN.12.5.03: precond for distinction still missing*)
5.55 @@ -124,13 +126,13 @@
5.56 e_rls, NONE, []));
5.57
5.58 store_pbt
5.59 - (prep_pbt (theory "DiffApp") "pbl_tool" [] e_pblID
5.60 + (prep_pbt thy "pbl_tool" [] e_pblID
5.61 (["tool"]:pblID,
5.62 [],
5.63 e_rls, NONE, []));
5.64
5.65 store_pbt
5.66 - (prep_pbt (theory "DiffApp") "pbl_tool_findvals" [] e_pblID
5.67 + (prep_pbt thy "pbl_tool_findvals" [] e_pblID
5.68 (["find_values","tool"]:pblID,
5.69 [("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_"]),
5.70 ("#Find" ,["valuesFor vls_"]),
5.71 @@ -142,14 +144,14 @@
5.72 (** methods, scripts not yet implemented **)
5.73
5.74 store_met
5.75 - (prep_met (theory "DiffApp") "met_diffapp" [] e_metID
5.76 + (prep_met thy "met_diffapp" [] e_metID
5.77 (["DiffApp"],
5.78 [],
5.79 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
5.80 crls = Atools_erls, nrls=norm_Rational
5.81 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
5.82 store_met
5.83 - (prep_met (theory "DiffApp") "met_diffapp_max" [] e_metID
5.84 + (prep_met thy "met_diffapp_max" [] e_metID
5.85 (["DiffApp","max_by_calculus"]:metID,
5.86 [("#Given" ,["fixedValues fix_","maximum m_","relations rs_",
5.87 "boundVariable v_","interval itv_","errorBound err_"]),
5.88 @@ -175,7 +177,7 @@
5.89 " bool_list_ (dropWhile (ident e_) rs_)])::bool list)) "
5.90 ));
5.91 store_met
5.92 - (prep_met (theory "DiffApp") "met_diffapp_funnew" [] e_metID
5.93 + (prep_met thy "met_diffapp_funnew" [] e_metID
5.94 (["DiffApp","make_fun_by_new_variable"]:metID,
5.95 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
5.96 ("#Find" ,["functionEq f_1_"])
5.97 @@ -200,7 +202,7 @@
5.98 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"
5.99 ));
5.100 store_met
5.101 -(prep_met (theory "DiffApp") "met_diffapp_funexp" [] e_metID
5.102 +(prep_met thy "met_diffapp_funexp" [] e_metID
5.103 (["DiffApp","make_fun_by_explicit"]:metID,
5.104 [("#Given" ,["functionOf f_","boundVariable v_","equalities eqs_"]),
5.105 ("#Find" ,["functionEq f_1_"])
5.106 @@ -220,7 +222,7 @@
5.107 " in Substitute [(v_1 = (rhs o hd) s_1)] h_) "
5.108 ));
5.109 store_met
5.110 - (prep_met (theory "DiffApp") "met_diffapp_max_oninterval" [] e_metID
5.111 + (prep_met thy "met_diffapp_max_oninterval" [] e_metID
5.112 (["DiffApp","max_on_interval_by_calculus"]:metID,
5.113 [("#Given" ,["functionEq t_","boundVariable v_","interval itv_"(*,
5.114 "errorBound err_"*)]),
5.115 @@ -232,7 +234,7 @@
5.116 "empty_script"
5.117 ));
5.118 store_met
5.119 - (prep_met (theory "DiffApp") "met_diffapp_findvals" [] e_metID
5.120 + (prep_met thy "met_diffapp_findvals" [] e_metID
5.121 (["DiffApp","find_values"]:metID,
5.122 [],
5.123 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls,
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 01 16:15:13 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Sep 01 16:43:58 2010 +0200
6.3 @@ -56,6 +56,8 @@
6.4 order_system_NxN "[a,b] = [b,a]"
6.5
6.6 ML {*
6.7 +val thy = @{theory};
6.8 +
6.9 (** eval functions **)
6.10
6.11 (*certain variables of a given list occur _all_ in a term
6.12 @@ -411,7 +413,7 @@
6.13 (** problems **)
6.14
6.15 store_pbt
6.16 - (prep_pbt (theory "EqSystem") "pbl_equsys" [] e_pblID
6.17 + (prep_pbt thy "pbl_equsys" [] e_pblID
6.18 (["system"],
6.19 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.20 ("#Find" ,["solution ss___"](*___ is copy-named*))
6.21 @@ -420,7 +422,7 @@
6.22 SOME "solveSystem es_ vs_",
6.23 []));
6.24 store_pbt
6.25 - (prep_pbt (theory "EqSystem") "pbl_equsys_lin" [] e_pblID
6.26 + (prep_pbt thy "pbl_equsys_lin" [] e_pblID
6.27 (["linear", "system"],
6.28 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.29 (*TODO.WN050929 check linearity*)
6.30 @@ -430,7 +432,7 @@
6.31 SOME "solveSystem es_ vs_",
6.32 []));
6.33 store_pbt
6.34 - (prep_pbt (theory "EqSystem") "pbl_equsys_lin_2x2" [] e_pblID
6.35 + (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID
6.36 (["2x2", "linear", "system"],
6.37 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.38 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.39 @@ -446,7 +448,7 @@
6.40 SOME "solveSystem es_ vs_",
6.41 []));
6.42 store_pbt
6.43 - (prep_pbt (theory "EqSystem") "pbl_equsys_lin_2x2_tri" [] e_pblID
6.44 + (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID
6.45 (["triangular", "2x2", "linear", "system"],
6.46 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.47 ("#Where" ,
6.48 @@ -458,7 +460,7 @@
6.49 SOME "solveSystem es_ vs_",
6.50 [["EqSystem","top_down_substitution","2x2"]]));
6.51 store_pbt
6.52 - (prep_pbt (theory "EqSystem") "pbl_equsys_lin_2x2_norm" [] e_pblID
6.53 + (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID
6.54 (["normalize", "2x2", "linear", "system"],
6.55 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.56 ("#Find" ,["solution ss___"])
6.57 @@ -467,7 +469,7 @@
6.58 SOME "solveSystem es_ vs_",
6.59 [["EqSystem","normalize","2x2"]]));
6.60 store_pbt
6.61 - (prep_pbt (theory "EqSystem") "pbl_equsys_lin_3x3" [] e_pblID
6.62 + (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID
6.63 (["3x3", "linear", "system"],
6.64 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.65 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.66 @@ -483,7 +485,7 @@
6.67 SOME "solveSystem es_ vs_",
6.68 []));
6.69 store_pbt
6.70 - (prep_pbt (theory "EqSystem") "pbl_equsys_lin_4x4" [] e_pblID
6.71 + (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID
6.72 (["4x4", "linear", "system"],
6.73 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
6.74 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.75 @@ -499,7 +501,7 @@
6.76 SOME "solveSystem es_ vs_",
6.77 []));
6.78 store_pbt
6.79 - (prep_pbt (theory "EqSystem") "pbl_equsys_lin_4x4_tri" [] e_pblID
6.80 + (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID
6.81 (["triangular", "4x4", "linear", "system"],
6.82 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.83 ("#Where" , (*accepts missing variables up to diagional form*)
6.84 @@ -516,7 +518,7 @@
6.85 [["EqSystem","top_down_substitution","4x4"]]));
6.86
6.87 store_pbt
6.88 - (prep_pbt (theory "EqSystem") "pbl_equsys_lin_4x4_norm" [] e_pblID
6.89 + (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID
6.90 (["normalize", "4x4", "linear", "system"],
6.91 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.92 (*length_ is checked 1 level above*)
6.93 @@ -533,7 +535,7 @@
6.94 (** methods **)
6.95
6.96 store_met
6.97 - (prep_met (theory "EqSystem") "met_eqsys" [] e_metID
6.98 + (prep_met thy "met_eqsys" [] e_metID
6.99 (["EqSystem"],
6.100 [],
6.101 {rew_ord'="tless_true", rls' = Erls, calc = [],
6.102 @@ -541,7 +543,7 @@
6.103 "empty_script"
6.104 ));
6.105 store_met
6.106 - (prep_met (theory "EqSystem") "met_eqsys_topdown" [] e_metID
6.107 + (prep_met thy "met_eqsys_topdown" [] e_metID
6.108 (["EqSystem","top_down_substitution"],
6.109 [],
6.110 {rew_ord'="tless_true", rls' = Erls, calc = [],
6.111 @@ -549,7 +551,7 @@
6.112 "empty_script"
6.113 ));
6.114 store_met
6.115 - (prep_met (theory "EqSystem") "met_eqsys_topdown_2x2" [] e_metID
6.116 + (prep_met thy "met_eqsys_topdown_2x2" [] e_metID
6.117 (["EqSystem","top_down_substitution","2x2"],
6.118 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.119 ("#Where" ,
6.120 @@ -599,7 +601,7 @@
6.121 ---------------------------------------------------------------------------*)
6.122 ));
6.123 store_met
6.124 - (prep_met (theory "EqSystem") "met_eqsys_norm" [] e_metID
6.125 + (prep_met thy "met_eqsys_norm" [] e_metID
6.126 (["EqSystem","normalize"],
6.127 [],
6.128 {rew_ord'="tless_true", rls' = Erls, calc = [],
6.129 @@ -607,7 +609,7 @@
6.130 "empty_script"
6.131 ));
6.132 store_met
6.133 - (prep_met (theory "EqSystem") "met_eqsys_norm_2x2" [] e_metID
6.134 + (prep_met thy "met_eqsys_norm_2x2" [] e_metID
6.135 (["EqSystem","normalize","2x2"],
6.136 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.137 ("#Find" ,["solution ss___"])],
6.138 @@ -647,7 +649,7 @@
6.139 Thm ("nth_Nil_",num_str @{thm nth_Nil_})],
6.140 scr = EmptyScr};
6.141 store_met
6.142 - (prep_met (theory "EqSystem") "met_eqsys_norm_4x4" [] e_metID
6.143 + (prep_met thy "met_eqsys_norm_4x4" [] e_metID
6.144 (["EqSystem","normalize","4x4"],
6.145 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.146 ("#Find" ,["solution ss___"])],
6.147 @@ -677,7 +679,7 @@
6.148 " [bool_list_ es__, real_list_ vs_]))"
6.149 ));
6.150 store_met
6.151 -(prep_met (theory "EqSystem") "met_eqsys_topdown_4x4" [] e_metID
6.152 +(prep_met thy "met_eqsys_topdown_4x4" [] e_metID
6.153 (["EqSystem","top_down_substitution","4x4"],
6.154 [("#Given" ,["equalities es_", "solveForVars vs_"]),
6.155 ("#Where" , (*accepts missing variables up to diagonal form*)
7.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Sep 01 16:15:13 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Sep 01 16:43:58 2010 +0200
7.3 @@ -28,6 +28,8 @@
7.4 (c) by Richard Lang, 2003 *}
7.5
7.6 ML {*
7.7 +val thy = @{theory};
7.8 +
7.9 val univariate_equation_prls =
7.10 append_rls "univariate_equation_prls" e_rls
7.11 [Calc ("Tools.matches",eval_matches "")];
7.12 @@ -38,7 +40,7 @@
7.13
7.14
7.15 store_pbt
7.16 - (prep_pbt (theory "Equation") "pbl_equ" [] e_pblID
7.17 + (prep_pbt thy "pbl_equ" [] e_pblID
7.18 (["equation"],
7.19 [("#Given" ,["equality e_","solveFor v_"]),
7.20 ("#Where" ,["matches (?a = ?b) e_"]),
7.21 @@ -50,7 +52,7 @@
7.22 []));
7.23
7.24 store_pbt
7.25 - (prep_pbt (theory "Equation") "pbl_equ_univ" [] e_pblID
7.26 + (prep_pbt thy "pbl_equ_univ" [] e_pblID
7.27 (["univariate","equation"],
7.28 [("#Given" ,["equality e_","solveFor v_"]),
7.29 ("#Where" ,["matches (?a = ?b) e_"]),
7.30 @@ -86,7 +88,7 @@
7.31
7.32
7.33 store_met
7.34 - (prep_met (theory "Equation") "met_equ" [] e_metID
7.35 + (prep_met thy "met_equ" [] e_metID
7.36 (["Equation"],
7.37 [],
7.38 {rew_ord'="tless_true", rls'=Erls, calc = [],
8.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 01 16:15:13 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 01 16:43:58 2010 +0200
8.3 @@ -45,6 +45,8 @@
8.4 integral_pow "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
8.5
8.6 ML {*
8.7 +val thy = @{theory};
8.8 +
8.9 (** eval functions **)
8.10
8.11 val c = Free ("c", HOLogic.realT);
8.12 @@ -330,7 +332,7 @@
8.13 (** problems **)
8.14
8.15 store_pbt
8.16 - (prep_pbt (theory "Integrate") "pbl_fun_integ" [] e_pblID
8.17 + (prep_pbt thy "pbl_fun_integ" [] e_pblID
8.18 (["integrate","function"],
8.19 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
8.20 ("#Find" ,["antiDerivative F_"])
8.21 @@ -341,7 +343,7 @@
8.22
8.23 (*here "named" is used differently from Differentiation"*)
8.24 store_pbt
8.25 - (prep_pbt (theory "Integrate") "pbl_fun_integ_nam" [] e_pblID
8.26 + (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
8.27 (["named","integrate","function"],
8.28 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
8.29 ("#Find" ,["antiDerivativeName F_"])
8.30 @@ -353,7 +355,7 @@
8.31 (** methods **)
8.32
8.33 store_met
8.34 - (prep_met (theory "Integrate") "met_diffint" [] e_metID
8.35 + (prep_met thy "met_diffint" [] e_metID
8.36 (["diff","integration"],
8.37 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
8.38 ("#Find" ,["antiDerivative F_"])
8.39 @@ -368,7 +370,7 @@
8.40 ));
8.41
8.42 store_met
8.43 - (prep_met (theory "Integrate") "met_diffint_named" [] e_metID
8.44 + (prep_met thy "met_diffint_named" [] e_metID
8.45 (["diff","integration","named"],
8.46 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
8.47 ("#Find" ,["antiDerivativeName F_"])
9.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Wed Sep 01 16:15:13 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Sep 01 16:43:58 2010 +0200
9.3 @@ -30,6 +30,8 @@
9.4 lin_isolate_div "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
9.5
9.6 ML {*
9.7 +val thy = @{theory};
9.8 +
9.9 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
9.10 append_rls "LinEq_prls" e_rls
9.11 [Calc ("op =",eval_equal "#equal_"),
9.12 @@ -124,7 +126,7 @@
9.13 *)
9.14 (* ---------linear----------- *)
9.15 store_pbt
9.16 - (prep_pbt (theory "LinEq") "pbl_equ_univ_lin" [] e_pblID
9.17 + (prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
9.18 (["linear","univariate","equation"],
9.19 [("#Given" ,["equality e_","solveFor v_"]),
9.20 ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*)
9.21 @@ -139,7 +141,7 @@
9.22
9.23 (*-------------- methods------------------------------------------------------*)
9.24 store_met
9.25 - (prep_met (theory "LinEq") "met_eqlin" [] e_metID
9.26 + (prep_met thy "met_eqlin" [] e_metID
9.27 (["LinEq"],
9.28 [],
9.29 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
9.30 @@ -148,7 +150,7 @@
9.31
9.32 (* ansprechen mit ["LinEq","solve_univar_equation"] *)
9.33 store_met
9.34 -(prep_met (theory "LinEq") "met_eq_lin" [] e_metID
9.35 +(prep_met thy "met_eq_lin" [] e_metID
9.36 (["LinEq","solve_lineq_equation"],
9.37 [("#Given" ,["equality e_","solveFor v_"]),
9.38 ("#Where" ,["Not( (lhs e_) is_polyrat_in v_)",
10.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Wed Sep 01 16:15:13 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Sep 01 16:43:58 2010 +0200
10.3 @@ -25,9 +25,11 @@
10.4 exp_invers_log "a^^^(a log b) = b"
10.5
10.6 ML {*
10.7 +val thy = @{theory};
10.8 +
10.9 (** problems **)
10.10 store_pbt
10.11 - (prep_pbt (theory "LogExp") "pbl_test_equ_univ_log" [] e_pblID
10.12 + (prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
10.13 (["logarithmic","univariate","equation"],
10.14 [("#Given",["equality e_","solveFor v_"]),
10.15 ("#Where",["matches ((?a log ?v_) = ?b) e_"]),
10.16 @@ -40,7 +42,7 @@
10.17
10.18 (** methods **)
10.19 store_met
10.20 - (prep_met (theory "LogExp") "met_equ_log" [] e_metID
10.21 + (prep_met thy "met_equ_log" [] e_metID
10.22 (["Equation","solve_log"],
10.23 [("#Given" ,["equality e_","solveFor v_"]),
10.24 ("#Where" ,["matches ((?a log ?v_) = ?b) e_"]),
11.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Sep 01 16:15:13 2010 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Sep 01 16:43:58 2010 +0200
11.3 @@ -170,6 +170,8 @@
11.4 *}
11.5
11.6 ML {*
11.7 +val thy = @{theory};
11.8 +
11.9 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
11.10 fun is_polyrat_in t v =
11.11 let fun coeff_in c v = member op = (vars c) v;
11.12 @@ -840,7 +842,7 @@
11.13 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
11.14 val order_add_mult =
11.15 Rls{id = "order_add_mult", preconds = [],
11.16 - rew_ord = ("ord_make_polynomial",ord_make_polynomial false (theory "Poly")),
11.17 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
11.18 erls = e_rls,srls = Erls,
11.19 calc = [],
11.20 (*asm_thm = [],*)
11.21 @@ -861,7 +863,7 @@
11.22 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
11.23 val order_mult =
11.24 Rls{id = "order_mult", preconds = [],
11.25 - rew_ord = ("ord_make_polynomial",ord_make_polynomial false (theory "Poly")),
11.26 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
11.27 erls = e_rls,srls = Erls,
11.28 calc = [],
11.29 (*asm_thm = [],*)
11.30 @@ -1395,7 +1397,7 @@
11.31 rew_ord = ("dummy_ord", dummy_ord),
11.32 erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*)
11.33 [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")
11.34 - (*WN.18.6.03 definiert in (theory "Poly"),
11.35 + (*WN.18.6.03 definiert in thy,
11.36 evaluiert prepat*)],
11.37 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
11.38 ("TIMES" ,("op *" ,eval_binop "#mult_")),
11.39 @@ -1593,7 +1595,7 @@
11.40 (** problems **)
11.41
11.42 store_pbt
11.43 - (prep_pbt (theory "Poly") "pbl_simp_poly" [] e_pblID
11.44 + (prep_pbt thy "pbl_simp_poly" [] e_pblID
11.45 (["polynomial","simplification"],
11.46 [("#Given" ,["TERM t_"]),
11.47 ("#Where" ,["t_ is_polyexp"]),
11.48 @@ -1608,7 +1610,7 @@
11.49 (** methods **)
11.50
11.51 store_met
11.52 - (prep_met (theory "Poly") "met_simp_poly" [] e_metID
11.53 + (prep_met thy "met_simp_poly" [] e_metID
11.54 (["simplification","for_polynomials"],
11.55 [("#Given" ,["TERM t_"]),
11.56 ("#Where" ,["t_ is_polyexp"]),
12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 01 16:15:13 2010 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 01 16:43:58 2010 +0200
12.3 @@ -362,6 +362,8 @@
12.4 separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
12.5
12.6 ML {*
12.7 +val thy = @{theory};
12.8 +
12.9 (*-------------------------rulse-------------------------*)
12.10 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
12.11 append_rls "PolyEq_prls" e_rls
12.12 @@ -828,7 +830,7 @@
12.13
12.14 (*-------------------------poly-----------------------*)
12.15 store_pbt
12.16 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly" [] e_pblID
12.17 + (prep_pbt thy "pbl_equ_univ_poly" [] e_pblID
12.18 (["polynomial","univariate","equation"],
12.19 [("#Given" ,["equality e_","solveFor v_"]),
12.20 ("#Where" ,["~((e_::bool) is_ratequation_in (v_::real))",
12.21 @@ -840,7 +842,7 @@
12.22 []));
12.23 (*--- d0 ---*)
12.24 store_pbt
12.25 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg0" [] e_pblID
12.26 + (prep_pbt thy "pbl_equ_univ_poly_deg0" [] e_pblID
12.27 (["degree_0","polynomial","univariate","equation"],
12.28 [("#Given" ,["equality e_","solveFor v_"]),
12.29 ("#Where" ,["matches (?a = 0) e_",
12.30 @@ -854,7 +856,7 @@
12.31
12.32 (*--- d1 ---*)
12.33 store_pbt
12.34 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg1" [] e_pblID
12.35 + (prep_pbt thy "pbl_equ_univ_poly_deg1" [] e_pblID
12.36 (["degree_1","polynomial","univariate","equation"],
12.37 [("#Given" ,["equality e_","solveFor v_"]),
12.38 ("#Where" ,["matches (?a = 0) e_",
12.39 @@ -868,7 +870,7 @@
12.40
12.41 (*--- d2 ---*)
12.42 store_pbt
12.43 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2" [] e_pblID
12.44 + (prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID
12.45 (["degree_2","polynomial","univariate","equation"],
12.46 [("#Given" ,["equality e_","solveFor v_"]),
12.47 ("#Where" ,["matches (?a = 0) e_",
12.48 @@ -880,7 +882,7 @@
12.49 [["PolyEq","solve_d2_polyeq_equation"]]));
12.50
12.51 store_pbt
12.52 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
12.53 + (prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
12.54 (["sq_only","degree_2","polynomial","univariate","equation"],
12.55 [("#Given" ,["equality e_","solveFor v_"]),
12.56 ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_ | " ^
12.57 @@ -901,7 +903,7 @@
12.58 [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
12.59
12.60 store_pbt
12.61 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
12.62 + (prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
12.63 (["bdv_only","degree_2","polynomial","univariate","equation"],
12.64 [("#Given" ,["equality e_","solveFor v_"]),
12.65 ("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_ | " ^
12.66 @@ -916,7 +918,7 @@
12.67 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
12.68
12.69 store_pbt
12.70 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_pq" [] e_pblID
12.71 + (prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID
12.72 (["pqFormula","degree_2","polynomial","univariate","equation"],
12.73 [("#Given" ,["equality e_","solveFor v_"]),
12.74 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_ | " ^
12.75 @@ -927,7 +929,7 @@
12.76 [["PolyEq","solve_d2_polyeq_pq_equation"]]));
12.77
12.78 store_pbt
12.79 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_abc" [] e_pblID
12.80 + (prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID
12.81 (["abcFormula","degree_2","polynomial","univariate","equation"],
12.82 [("#Given" ,["equality e_","solveFor v_"]),
12.83 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_ | " ^
12.84 @@ -939,7 +941,7 @@
12.85
12.86 (*--- d3 ---*)
12.87 store_pbt
12.88 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg3" [] e_pblID
12.89 + (prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID
12.90 (["degree_3","polynomial","univariate","equation"],
12.91 [("#Given" ,["equality e_","solveFor v_"]),
12.92 ("#Where" ,["matches (?a = 0) e_",
12.93 @@ -952,7 +954,7 @@
12.94
12.95 (*--- d4 ---*)
12.96 store_pbt
12.97 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg4" [] e_pblID
12.98 + (prep_pbt thy "pbl_equ_univ_poly_deg4" [] e_pblID
12.99 (["degree_4","polynomial","univariate","equation"],
12.100 [("#Given" ,["equality e_","solveFor v_"]),
12.101 ("#Where" ,["matches (?a = 0) e_",
12.102 @@ -965,7 +967,7 @@
12.103
12.104 (*--- normalize ---*)
12.105 store_pbt
12.106 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_norm" [] e_pblID
12.107 + (prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID
12.108 (["normalize","polynomial","univariate","equation"],
12.109 [("#Given" ,["equality e_","solveFor v_"]),
12.110 ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |" ^
12.111 @@ -976,7 +978,7 @@
12.112 [["PolyEq","normalize_poly"]]));
12.113 (*-------------------------expanded-----------------------*)
12.114 store_pbt
12.115 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_expand" [] e_pblID
12.116 + (prep_pbt thy "pbl_equ_univ_expand" [] e_pblID
12.117 (["expanded","univariate","equation"],
12.118 [("#Given" ,["equality e_","solveFor v_"]),
12.119 ("#Where" ,["matches (?a = 0) e_",
12.120 @@ -988,7 +990,7 @@
12.121
12.122 (*--- d2 ---*)
12.123 store_pbt
12.124 - (prep_pbt (theory "PolyEq") "pbl_equ_univ_expand_deg2" [] e_pblID
12.125 + (prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID
12.126 (["degree_2","expanded","univariate","equation"],
12.127 [("#Given" ,["equality e_","solveFor v_"]),
12.128 ("#Where" ,["((lhs e_) has_degree_in v_) = 2"]),
12.129 @@ -1000,14 +1002,14 @@
12.130
12.131 "-------------------------methods-----------------------";
12.132 store_met
12.133 - (prep_met (theory "PolyEq") "met_polyeq" [] e_metID
12.134 + (prep_met thy "met_polyeq" [] e_metID
12.135 (["PolyEq"],
12.136 [],
12.137 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
12.138 crls=PolyEq_crls, nrls=norm_Rational}, "empty_script"));
12.139
12.140 store_met
12.141 - (prep_met (theory "PolyEq") "met_polyeq_norm" [] e_metID
12.142 + (prep_met thy "met_polyeq_norm" [] e_metID
12.143 (["PolyEq","normalize_poly"],
12.144 [("#Given" ,["equality e_","solveFor v_"]),
12.145 ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |" ^
12.146 @@ -1032,7 +1034,7 @@
12.147 ));
12.148
12.149 store_met
12.150 - (prep_met (theory "PolyEq") "met_polyeq_d0" [] e_metID
12.151 + (prep_met thy "met_polyeq_d0" [] e_metID
12.152 (["PolyEq","solve_d0_polyeq_equation"],
12.153 [("#Given" ,["equality e_","solveFor v_"]),
12.154 ("#Where" ,["(lhs e_) is_poly_in v_ ",
12.155 @@ -1052,7 +1054,7 @@
12.156 ));
12.157
12.158 store_met
12.159 - (prep_met (theory "PolyEq") "met_polyeq_d1" [] e_metID
12.160 + (prep_met thy "met_polyeq_d1" [] e_metID
12.161 (["PolyEq","solve_d1_polyeq_equation"],
12.162 [("#Given" ,["equality e_","solveFor v_"]),
12.163 ("#Where" ,["(lhs e_) is_poly_in v_ ",
12.164 @@ -1078,7 +1080,7 @@
12.165 ));
12.166
12.167 store_met
12.168 - (prep_met (theory "PolyEq") "met_polyeq_d22" [] e_metID
12.169 + (prep_met thy "met_polyeq_d22" [] e_metID
12.170 (["PolyEq","solve_d2_polyeq_equation"],
12.171 [("#Given" ,["equality e_","solveFor v_"]),
12.172 ("#Where" ,["(lhs e_) is_poly_in v_ ",
12.173 @@ -1104,7 +1106,7 @@
12.174 ));
12.175
12.176 store_met
12.177 - (prep_met (theory "PolyEq") "met_polyeq_d2_bdvonly" [] e_metID
12.178 + (prep_met thy "met_polyeq_d2_bdvonly" [] e_metID
12.179 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
12.180 [("#Given" ,["equality e_","solveFor v_"]),
12.181 ("#Where" ,["(lhs e_) is_poly_in v_ ",
12.182 @@ -1130,7 +1132,7 @@
12.183 ));
12.184
12.185 store_met
12.186 - (prep_met (theory "PolyEq") "met_polyeq_d2_sqonly" [] e_metID
12.187 + (prep_met thy "met_polyeq_d2_sqonly" [] e_metID
12.188 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
12.189 [("#Given" ,["equality e_","solveFor v_"]),
12.190 ("#Where" ,["(lhs e_) is_poly_in v_ ",
12.191 @@ -1153,7 +1155,7 @@
12.192 ));
12.193
12.194 store_met
12.195 - (prep_met (theory "PolyEq") "met_polyeq_d2_pq" [] e_metID
12.196 + (prep_met thy "met_polyeq_d2_pq" [] e_metID
12.197 (["PolyEq","solve_d2_polyeq_pq_equation"],
12.198 [("#Given" ,["equality e_","solveFor v_"]),
12.199 ("#Where" ,["(lhs e_) is_poly_in v_ ",
12.200 @@ -1176,7 +1178,7 @@
12.201 ));
12.202
12.203 store_met
12.204 - (prep_met (theory "PolyEq") "met_polyeq_d2_abc" [] e_metID
12.205 + (prep_met thy "met_polyeq_d2_abc" [] e_metID
12.206 (["PolyEq","solve_d2_polyeq_abc_equation"],
12.207 [("#Given" ,["equality e_","solveFor v_"]),
12.208 ("#Where" ,["(lhs e_) is_poly_in v_ ",
12.209 @@ -1199,7 +1201,7 @@
12.210 ));
12.211
12.212 store_met
12.213 - (prep_met (theory "PolyEq") "met_polyeq_d3" [] e_metID
12.214 + (prep_met thy "met_polyeq_d3" [] e_metID
12.215 (["PolyEq","solve_d3_polyeq_equation"],
12.216 [("#Given" ,["equality e_","solveFor v_"]),
12.217 ("#Where" ,["(lhs e_) is_poly_in v_ ",
12.218 @@ -1231,7 +1233,7 @@
12.219 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
12.220 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
12.221 store_met
12.222 - (prep_met (theory "PolyEq") "met_polyeq_complsq" [] e_metID
12.223 + (prep_met thy "met_polyeq_complsq" [] e_metID
12.224 (["PolyEq","complete_square"],
12.225 [("#Given" ,["equality e_","solveFor v_"]),
12.226 ("#Where" ,["matches (?a = 0) e_",
13.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Sep 01 16:15:13 2010 +0200
13.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Wed Sep 01 16:43:58 2010 +0200
13.3 @@ -106,6 +106,8 @@
13.4 klammer_minus_mult "(b - c) * a = b * a - c * a"
13.5
13.6 ML {*
13.7 +val thy = @{theory};
13.8 +
13.9 (** eval functions **)
13.10
13.11 (*. get the identifier from specific monomials; see fun ist_monom .*)
13.12 @@ -398,12 +400,12 @@
13.13 (** problems **)
13.14
13.15 store_pbt
13.16 - (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly" [] e_pblID
13.17 + (prep_pbt thy "pbl_vereinf_poly" [] e_pblID
13.18 (["polynom","vereinfachen"],
13.19 [], Erls, NONE, []));
13.20
13.21 store_pbt
13.22 - (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_minus" [] e_pblID
13.23 + (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID
13.24 (["plus_minus","polynom","vereinfachen"],
13.25 [("#Given" ,["TERM t_"]),
13.26 ("#Where" ,["t_ is_polyexp",
13.27 @@ -432,7 +434,7 @@
13.28 [["simplification","for_polynomials","with_minus"]]));
13.29
13.30 store_pbt
13.31 - (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_klammer" [] e_pblID
13.32 + (prep_pbt thy "pbl_vereinf_poly_klammer" [] e_pblID
13.33 (["klammer","polynom","vereinfachen"],
13.34 [("#Given" ,["TERM t_"]),
13.35 ("#Where" ,["t_ is_polyexp",
13.36 @@ -456,7 +458,7 @@
13.37 [["simplification","for_polynomials","with_parentheses"]]));
13.38
13.39 store_pbt
13.40 - (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_klammer_mal" [] e_pblID
13.41 + (prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
13.42 (["binom_klammer","polynom","vereinfachen"],
13.43 [("#Given" ,["TERM t_"]),
13.44 ("#Where" ,["t_ is_polyexp"]),
13.45 @@ -468,12 +470,12 @@
13.46 [["simplification","for_polynomials","with_parentheses_mult"]]));
13.47
13.48 store_pbt
13.49 - (prep_pbt (theory "PolyMinus") "pbl_probe" [] e_pblID
13.50 + (prep_pbt thy "pbl_probe" [] e_pblID
13.51 (["probe"],
13.52 [], Erls, NONE, []));
13.53
13.54 store_pbt
13.55 - (prep_pbt (theory "PolyMinus") "pbl_probe_poly" [] e_pblID
13.56 + (prep_pbt thy "pbl_probe_poly" [] e_pblID
13.57 (["polynom","probe"],
13.58 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
13.59 ("#Where" ,["e_ is_polyexp"]),
13.60 @@ -486,7 +488,7 @@
13.61 [["probe","fuer_polynom"]]));
13.62
13.63 store_pbt
13.64 - (prep_pbt (theory "PolyMinus") "pbl_probe_bruch" [] e_pblID
13.65 + (prep_pbt thy "pbl_probe_bruch" [] e_pblID
13.66 (["bruch","probe"],
13.67 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
13.68 ("#Where" ,["e_ is_ratpolyexp"]),
13.69 @@ -502,7 +504,7 @@
13.70 (** methods **)
13.71
13.72 store_met
13.73 - (prep_met (theory "PolyMinus") "met_simp_poly_minus" [] e_metID
13.74 + (prep_met thy "met_simp_poly_minus" [] e_metID
13.75 (["simplification","for_polynomials","with_minus"],
13.76 [("#Given" ,["TERM t_"]),
13.77 ("#Where" ,["t_ is_polyexp",
13.78 @@ -532,7 +534,7 @@
13.79 ));
13.80
13.81 store_met
13.82 - (prep_met (theory "PolyMinus") "met_simp_poly_parenth" [] e_metID
13.83 + (prep_met thy "met_simp_poly_parenth" [] e_metID
13.84 (["simplification","for_polynomials","with_parentheses"],
13.85 [("#Given" ,["TERM t_"]),
13.86 ("#Where" ,["t_ is_polyexp"]),
13.87 @@ -551,7 +553,7 @@
13.88 ));
13.89
13.90 store_met
13.91 - (prep_met (theory "PolyMinus") "met_simp_poly_parenth_mult" [] e_metID
13.92 + (prep_met thy "met_simp_poly_parenth_mult" [] e_metID
13.93 (["simplification","for_polynomials","with_parentheses_mult"],
13.94 [("#Given" ,["TERM t_"]),
13.95 ("#Where" ,["t_ is_polyexp"]),
13.96 @@ -573,7 +575,7 @@
13.97 ));
13.98
13.99 store_met
13.100 - (prep_met (theory "PolyMinus") "met_probe" [] e_metID
13.101 + (prep_met thy "met_probe" [] e_metID
13.102 (["probe"],
13.103 [],
13.104 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
13.105 @@ -581,7 +583,7 @@
13.106 "empty_script"));
13.107
13.108 store_met
13.109 - (prep_met (theory "PolyMinus") "met_probe_poly" [] e_metID
13.110 + (prep_met thy "met_probe_poly" [] e_metID
13.111 (["probe","fuer_polynom"],
13.112 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
13.113 ("#Where" ,["e_ is_polyexp"]),
13.114 @@ -602,7 +604,7 @@
13.115 ));
13.116
13.117 store_met
13.118 - (prep_met (theory "PolyMinus") "met_probe_bruch" [] e_metID
13.119 + (prep_met thy "met_probe_bruch" [] e_metID
13.120 (["probe","fuer_bruch"],
13.121 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
13.122 ("#Where" ,["e_ is_ratpolyexp"]),
14.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Wed Sep 01 16:15:13 2010 +0200
14.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Sep 01 16:43:58 2010 +0200
14.3 @@ -49,6 +49,8 @@
14.4 "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
14.5
14.6 ML {*
14.7 +val thy = @{theory};
14.8 +
14.9 (*-------------------------functions-----------------------*)
14.10 (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
14.11 fun is_rateqation_in t v =
14.12 @@ -175,7 +177,7 @@
14.13 show_ptyps();
14.14 *)
14.15 store_pbt
14.16 - (prep_pbt (theory "RatEq") "pbl_equ_univ_rat" [] e_pblID
14.17 + (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
14.18 (["rational","univariate","equation"],
14.19 [("#Given" ,["equality e_","solveFor v_"]),
14.20 ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),
14.21 @@ -188,14 +190,14 @@
14.22
14.23 (*-------------------------methods-----------------------*)
14.24 store_met
14.25 - (prep_met (theory "RatEq") "met_rateq" [] e_metID
14.26 + (prep_met thy "met_rateq" [] e_metID
14.27 (["RatEq"],
14.28 [],
14.29 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
14.30 crls=RatEq_crls, nrls=norm_Rational
14.31 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
14.32 store_met
14.33 - (prep_met (theory "RatEq") "met_rat_eq" [] e_metID
14.34 + (prep_met thy "met_rat_eq" [] e_metID
14.35 (["RatEq","solve_rat_equation"],
14.36 [("#Given" ,["equality e_","solveFor v_"]),
14.37 ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]),
15.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Sep 01 16:15:13 2010 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Sep 01 16:43:58 2010 +0200
15.3 @@ -86,6 +86,8 @@
15.4 *}
15.5
15.6 ML {*
15.7 +val thy = @{theory};
15.8 +
15.9 signature RATIONALI =
15.10 sig
15.11 type mv_monom
15.12 @@ -2886,8 +2888,6 @@
15.13 val {rules, rew_ord=(_,ro),...} =
15.14 rep_rls (assoc_rls "rev_rew_p");
15.15
15.16 -val thy = (theory "Rational");
15.17 -
15.18 (*.init_state = fn : term -> istate
15.19 initialzies the state of the script interpreter. The state is:
15.20
15.21 @@ -2904,7 +2904,7 @@
15.22 (#) could be extracted from here by (map #1)*).*)
15.23 (* val {rules, rew_ord=(_,ro),...} =
15.24 rep_rls (assoc_rls "rev_rew_p") (*USE ALWAYS, SEE val cancel_p*);
15.25 - val (thy, eval_rls, ro) =((theory "Rational"), Atools_erls, ro) (*..val cancel_p*);
15.26 + val (thy, eval_rls, ro) =(thy, Atools_erls, ro) (*..val cancel_p*);
15.27 val t = t;
15.28 *)
15.29 fun init_state thy eval_rls ro t =
15.30 @@ -2961,12 +2961,12 @@
15.31 value:
15.32 -> rule option: ... this rule is appropriate for cancellation;
15.33 there may be no such rule (if the term is canceled already.*)
15.34 -(* val thy = (theory "Rational");
15.35 +(* val thy = thy;
15.36 val Rrls {rew_ord=(_,ro),...} = cancel;
15.37 val ([rs],t) = (rss,f);
15.38 next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)
15.39
15.40 - val (thy, [rs]) = ((theory "Rational"), revsets);
15.41 + val (thy, [rs]) = (thy, revsets);
15.42 val Rrls {rew_ord=(_,ro),...} = cancel;
15.43 nex [rs] t;
15.44 *)
15.45 @@ -3003,7 +3003,7 @@
15.46 val cancel_p =
15.47 Rrls {id = "cancel_p", prepat=[],
15.48 rew_ord=("ord_make_polynomial",
15.49 - ord_make_polynomial false (theory "Rational")),
15.50 + ord_make_polynomial false thy),
15.51 erls = rational_erls,
15.52 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
15.53 ("TIMES" ,("op *" ,eval_binop "#mult_")),
15.54 @@ -3036,7 +3036,7 @@
15.55 *)
15.56 val {rules=rules,rew_ord=(_,ro),...} =
15.57 rep_rls (assoc_rls "expand_binoms");
15.58 -val thy = (theory "Rational");
15.59 +val thy = thy;
15.60
15.61 fun init_state thy eval_rls ro t =
15.62 let val SOME (t',_) = factout_ thy t;
15.63 @@ -3086,7 +3086,7 @@
15.64 val cancel =
15.65 Rrls {id = "cancel", prepat=prepat,
15.66 rew_ord=("ord_make_polynomial",
15.67 - ord_make_polynomial false (theory "Rational")),
15.68 + ord_make_polynomial false thy),
15.69 erls = rational_erls,
15.70 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
15.71 ("TIMES" ,("op *" ,eval_binop "#mult_")),
15.72 @@ -3112,7 +3112,7 @@
15.73 see rational.sml --- investigate rulesets for cancel_p ---*)
15.74 val {rules, rew_ord=(_,ro),...} =
15.75 rep_rls (assoc_rls "rev_rew_p");
15.76 -val thy = (theory "Rational");
15.77 +val thy = thy;
15.78
15.79
15.80 (*.common_nominator_p_ = fn : theory -> term -> (term * term list) option
15.81 @@ -3188,12 +3188,12 @@
15.82 value:
15.83 -> rule option: ... this rule is appropriate for cancellation;
15.84 there may be no such rule (if the term is canceled already.*)
15.85 -(* val thy = (theory "Rational");
15.86 +(* val thy = thy;
15.87 val Rrls {rew_ord=(_,ro),...} = cancel;
15.88 val ([rs],t) = (rss,f);
15.89 next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)
15.90
15.91 - val (thy, [rs]) = ((theory "Rational"), revsets);
15.92 + val (thy, [rs]) = (thy, revsets);
15.93 val Rrls {rew_ord=(_,ro),...} = cancel;
15.94 nex [rs] t;
15.95 *)
15.96 @@ -3240,7 +3240,7 @@
15.97 val common_nominator_p =
15.98 Rrls {id = "common_nominator_p", prepat=prepat,
15.99 rew_ord=("ord_make_polynomial",
15.100 - ord_make_polynomial false (theory "Rational")),
15.101 + ord_make_polynomial false thy),
15.102 erls = rational_erls,
15.103 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
15.104 ("TIMES" ,("op *" ,eval_binop "#mult_")),
15.105 @@ -3261,7 +3261,7 @@
15.106
15.107 val {rules=rules,rew_ord=(_,ro),...} =
15.108 rep_rls (assoc_rls "make_polynomial");
15.109 -val thy = (theory "Rational");
15.110 +val thy = thy;
15.111
15.112
15.113 (*.common_nominator_ = fn : theory -> term -> (term * term list) option
15.114 @@ -3337,12 +3337,12 @@
15.115 value:
15.116 -> rule option: ... this rule is appropriate for cancellation;
15.117 there may be no such rule (if the term is canceled already.*)
15.118 -(* val thy = (theory "Rational");
15.119 +(* val thy = thy;
15.120 val Rrls {rew_ord=(_,ro),...} = cancel;
15.121 val ([rs],t) = (rss,f);
15.122 next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)
15.123
15.124 - val (thy, [rs]) = ((theory "Rational"), revsets);
15.125 + val (thy, [rs]) = (thy, revsets);
15.126 val Rrls {rew_ord=(_,ro),...} = cancel_p;
15.127 nex [rs] t;
15.128 *)
15.129 @@ -3393,7 +3393,7 @@
15.130 val common_nominator =
15.131 Rrls {id = "common_nominator", prepat=prepat,
15.132 rew_ord=("ord_make_polynomial",
15.133 - ord_make_polynomial false (theory "Rational")),
15.134 + ord_make_polynomial false thy),
15.135 erls = rational_erls,
15.136 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
15.137 ("TIMES" ,("op *" ,eval_binop "#mult_")),
15.138 @@ -3794,7 +3794,7 @@
15.139 (** problems **)
15.140
15.141 store_pbt
15.142 - (prep_pbt (theory "Rational") "pbl_simp_rat" [] e_pblID
15.143 + (prep_pbt thy "pbl_simp_rat" [] e_pblID
15.144 (["rational","simplification"],
15.145 [("#Given" ,["TERM t_"]),
15.146 ("#Where" ,["t_ is_ratpolyexp"]),
15.147 @@ -3809,7 +3809,7 @@
15.148 (*WN061025 this methods script is copied from (auto-generated) script
15.149 of norm_Rational in order to ease repair on inform*)
15.150 store_met
15.151 - (prep_met (theory "Rational") "met_simp_rat" [] e_metID
15.152 + (prep_met thy "met_simp_rat" [] e_metID
15.153 (["simplification","of_rationals"],
15.154 [("#Given" ,["TERM t_"]),
15.155 ("#Where" ,["t_ is_ratpolyexp"]),
16.1 --- a/src/Tools/isac/Knowledge/Root.thy Wed Sep 01 16:15:13 2010 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Sep 01 16:43:58 2010 +0200
16.3 @@ -42,6 +42,8 @@
16.4 real_root_negative "a < 0 ==> (x ^^^ 2 = a) = False"
16.5
16.6 ML {*
16.7 +val thy = @{theory};
16.8 +
16.9 (*-------------------------functions---------------------*)
16.10 (*evaluation square-root over the integers*)
16.11 fun eval_sqrt (thmid:string) (op_:string) (t as
16.12 @@ -191,7 +193,7 @@
16.13
16.14 val make_rooteq = prep_rls(
16.15 Rls{id = "make_rooteq", preconds = []:term list,
16.16 - rew_ord = ("sqrt_right", sqrt_right false (theory "Root")),
16.17 + rew_ord = ("sqrt_right", sqrt_right false thy),
16.18 erls = Atools_erls, srls = Erls,
16.19 calc = [],
16.20 (*asm_thm = [],*)
17.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Wed Sep 01 16:15:13 2010 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Sep 01 16:43:58 2010 +0200
17.3 @@ -118,6 +118,8 @@
17.4 ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
17.5
17.6 ML {*
17.7 +val thy = @{theory};
17.8 +
17.9 (*-------------------------functions---------------------*)
17.10 (* true if bdv is under sqrt of a Equation*)
17.11 fun is_rootTerm_in t v =
17.12 @@ -475,7 +477,7 @@
17.13 *)
17.14 (* ---------root----------- *)
17.15 store_pbt
17.16 - (prep_pbt (theory "RootEq") "pbl_equ_univ_root" [] e_pblID
17.17 + (prep_pbt thy "pbl_equ_univ_root" [] e_pblID
17.18 (["root","univariate","equation"],
17.19 [("#Given" ,["equality e_","solveFor v_"]),
17.20 ("#Where" ,["(lhs e_) is_rootTerm_in (v_::real) | " ^
17.21 @@ -486,7 +488,7 @@
17.22 []));
17.23 (* ---------sqrt----------- *)
17.24 store_pbt
17.25 - (prep_pbt (theory "RootEq") "pbl_equ_univ_root_sq" [] e_pblID
17.26 + (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID
17.27 (["sq","root","univariate","equation"],
17.28 [("#Given" ,["equality e_","solveFor v_"]),
17.29 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
17.30 @@ -499,7 +501,7 @@
17.31 [["RootEq","solve_sq_root_equation"]]));
17.32 (* ---------normalize----------- *)
17.33 store_pbt
17.34 - (prep_pbt (theory "RootEq") "pbl_equ_univ_root_norm" [] e_pblID
17.35 + (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID
17.36 (["normalize","root","univariate","equation"],
17.37 [("#Given" ,["equality e_","solveFor v_"]),
17.38 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
17.39 @@ -514,7 +516,7 @@
17.40 (*-------------------------methods-----------------------*)
17.41 (* ---- root 20.8.02 ---*)
17.42 store_met
17.43 - (prep_met (theory "RootEq") "met_rooteq" [] e_metID
17.44 + (prep_met thy "met_rooteq" [] e_metID
17.45 (["RootEq"],
17.46 [],
17.47 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
17.48 @@ -522,7 +524,7 @@
17.49 asm_rls=[],asm_thm=[]*)}, "empty_script"));
17.50 (*-- normalize 20.10.02 --*)
17.51 store_met
17.52 - (prep_met (theory "RootEq") "met_rooteq_norm" [] e_metID
17.53 + (prep_met thy "met_rooteq_norm" [] e_metID
17.54 (["RootEq","norm_sq_root_equation"],
17.55 [("#Given" ,["equality e_","solveFor v_"]),
17.56 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
17.57 @@ -550,7 +552,7 @@
17.58 ));
17.59
17.60 store_met
17.61 - (prep_met (theory "RootEq") "met_rooteq_sq" [] e_metID
17.62 + (prep_met thy "met_rooteq_sq" [] e_metID
17.63 (["RootEq","solve_sq_root_equation"],
17.64 [("#Given" ,["equality e_","solveFor v_"]),
17.65 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
17.66 @@ -583,7 +585,7 @@
17.67
17.68 (*-- right 28.08.02 --*)
17.69 store_met
17.70 - (prep_met (theory "RootEq") "met_rooteq_sq_right" [] e_metID
17.71 + (prep_met thy "met_rooteq_sq_right" [] e_metID
17.72 (["RootEq","solve_right_sq_root_equation"],
17.73 [("#Given" ,["equality e_","solveFor v_"]),
17.74 ("#Where" ,["(rhs e_) is_sqrtTerm_in v_"]),
17.75 @@ -611,7 +613,7 @@
17.76
17.77 (*-- left 28.08.02 --*)
17.78 store_met
17.79 - (prep_met (theory "RootEq") "met_rooteq_sq_left" [] e_metID
17.80 + (prep_met thy "met_rooteq_sq_left" [] e_metID
17.81 (["RootEq","solve_left_sq_root_equation"],
17.82 [("#Given" ,["equality e_","solveFor v_"]),
17.83 ("#Where" ,["(lhs e_) is_sqrtTerm_in v_"]),
18.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Wed Sep 01 16:15:13 2010 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Wed Sep 01 16:43:58 2010 +0200
18.3 @@ -10,6 +10,8 @@
18.4 theory RootRat imports Root Rational begin
18.5
18.6 ML {*
18.7 +val thy = @{theory};
18.8 +
18.9 (*-------------------------rules-------------------------*)
18.10 val rootrat_erls =
18.11 merge_rls "rootrat_erls" Root_erls
18.12 @@ -17,7 +19,7 @@
18.13 (append_rls "" e_rls
18.14 []));
18.15
18.16 -ruleset' := overwritelthy @{theory} (!ruleset',
18.17 +ruleset' := overwritelthy thy (!ruleset',
18.18 [("rootrat_erls",rootrat_erls) (*FIXXXME:del with rls.rls'*)]);
18.19
18.20 (*.calculate numeral groundterms.*)
18.21 @@ -32,7 +34,7 @@
18.22 (* "- z1 = -1 * z1" *)
18.23 Calc ("Root.sqrt",eval_sqrt "#sqrt_")
18.24 ];
18.25 -ruleset' := overwritelthy @{theory} (!ruleset',
18.26 +ruleset' := overwritelthy thy (!ruleset',
18.27 [("calculate_RootRat",calculate_RootRat)]);
18.28 *}
18.29
19.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Wed Sep 01 16:15:13 2010 +0200
19.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed Sep 01 16:43:58 2010 +0200
19.3 @@ -34,6 +34,8 @@
19.4 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
19.5
19.6 ML {*
19.7 +val thy = @{theory};
19.8 +
19.9 (*-------------------------functions---------------------*)
19.10 (* true if denominator contains (sq)root in + or - term
19.11 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true
19.12 @@ -130,8 +132,9 @@
19.13 (get_pbt ["rat","root","univariate","equation"]);
19.14 show_ptyps();
19.15 *)
19.16 +
19.17 store_pbt
19.18 - (prep_pbt (theory "RootRatEq") "pbl_equ_univ_root_sq_rat" [] e_pblID
19.19 + (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
19.20 (["rat","sq","root","univariate","equation"],
19.21 [("#Given" ,["equality e_","solveFor v_"]),
19.22 ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) )| " ^
19.23 @@ -150,7 +153,7 @@
19.24 crls=Atools_erls, nrls=norm_Rational}, "empty_script"));
19.25 (*-- left 20.10.02 --*)
19.26 store_met
19.27 - (prep_met (theory "RootRatEq") "met_rootrateq_elim" [] e_metID
19.28 + (prep_met thy "met_rootrateq_elim" [] e_metID
19.29 (["RootRatEq","elim_rootrat_equation"],
19.30 [("#Given" ,["equality e_","solveFor v_"]),
19.31 ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) ) | " ^
20.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Wed Sep 01 16:15:13 2010 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Wed Sep 01 16:43:58 2010 +0200
20.3 @@ -19,13 +19,12 @@
20.4 SimplifyScript :: "[real, real] => real"
20.5 ("((Script SimplifyScript (_ =))// (_))" 9)
20.6
20.7 -ML {* "ok" *}
20.8 -
20.9 ML {*
20.10 +val thy = @{theory};
20.11
20.12 (** problems **)
20.13 store_pbt
20.14 - (prep_pbt @{theory} "pbl_simp" [] e_pblID
20.15 + (prep_pbt thy "pbl_simp" [] e_pblID
20.16 (["simplification"],
20.17 [("#Given" ,["TERM t_t"]),
20.18 ("#Find" ,["normalform n_n"])
20.19 @@ -35,7 +34,7 @@
20.20 []));
20.21
20.22 store_pbt
20.23 - (prep_pbt @{theory} "pbl_vereinfache" [] e_pblID
20.24 + (prep_pbt thy "pbl_vereinfache" [] e_pblID
20.25 (["vereinfachen"],
20.26 [("#Given" ,["TERM t_t"]),
20.27 ("#Find" ,["normalform n_n"])
20.28 @@ -47,7 +46,7 @@
20.29 (** methods **)
20.30
20.31 store_met
20.32 - (prep_met @{theory} "met_tsimp" [] e_metID
20.33 + (prep_met thy "met_tsimp" [] e_metID
20.34 (["simplification"],
20.35 [("#Given" ,["TERM t_t"]),
20.36 ("#Find" ,["normalform n_n"])
20.37 @@ -70,18 +69,18 @@
20.38 "Simplify (2*a + 3*a)");
20.39 *)
20.40 fun argl2dtss t =
20.41 - [((term_of o the o (parse @{theory})) "TERM", t),
20.42 - ((term_of o the o (parse @{theory})) "normalform",
20.43 - [(term_of o the o (parse @{theory})) "N"])
20.44 + [((term_of o the o (parse thy)) "TERM", t),
20.45 + ((term_of o the o (parse thy)) "normalform",
20.46 + [(term_of o the o (parse thy)) "N"])
20.47 ]
20.48 | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";
20.49
20.50 castab :=
20.51 overwritel (!castab,
20.52 - [((term_of o the o (parse @{theory})) "Simplify",
20.53 + [((term_of o the o (parse thy)) "Simplify",
20.54 (("Isac", ["simplification"], ["no_met"]),
20.55 argl2dtss)),
20.56 - ((term_of o the o (parse @{theory})) "Vereinfache",
20.57 + ((term_of o the o (parse thy)) "Vereinfache",
20.58 (("Isac", ["vereinfachen"], ["no_met"]),
20.59 argl2dtss))
20.60 ]);
21.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Sep 01 16:15:13 2010 +0200
21.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Sep 01 16:43:58 2010 +0200
21.3 @@ -166,6 +166,8 @@
21.4 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)
21.5
21.6 ML {*
21.7 +val thy = @{theory};
21.8 +
21.9 (** evaluation of numerals and predicates **)
21.10
21.11 (*does a term contain a root ?*)
21.12 @@ -507,12 +509,12 @@
21.13
21.14 (** problem types **)
21.15 store_pbt
21.16 - (prep_pbt (theory "Test") "pbl_test" [] e_pblID
21.17 + (prep_pbt thy "pbl_test" [] e_pblID
21.18 (["test"],
21.19 [],
21.20 e_rls, NONE, []));
21.21 store_pbt
21.22 - (prep_pbt (theory "Test") "pbl_test_equ" [] e_pblID
21.23 + (prep_pbt thy "pbl_test_equ" [] e_pblID
21.24 (["equation","test"],
21.25 [("#Given" ,["equality e_","solveFor v_"]),
21.26 ("#Where" ,["matches (?a = ?b) e_"]),
21.27 @@ -522,7 +524,7 @@
21.28 SOME "solve (e_::bool, v_)", []));
21.29
21.30 store_pbt
21.31 - (prep_pbt (theory "Test") "pbl_test_uni" [] e_pblID
21.32 + (prep_pbt thy "pbl_test_uni" [] e_pblID
21.33 (["univariate","equation","test"],
21.34 [("#Given" ,["equality e_","solveFor v_"]),
21.35 ("#Where" ,["matches (?a = ?b) e_"]),
21.36 @@ -532,7 +534,7 @@
21.37 SOME "solve (e_::bool, v_)", []));
21.38
21.39 store_pbt
21.40 - (prep_pbt (theory "Test") "pbl_test_uni_lin" [] e_pblID
21.41 + (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
21.42 (["linear","univariate","equation","test"],
21.43 [("#Given" ,["equality e_","solveFor v_"]),
21.44 ("#Where" ,["(matches ( v_ = 0) e_) | (matches ( ?b*v_ = 0) e_) |" ^
21.45 @@ -544,16 +546,16 @@
21.46
21.47 (*25.8.01 ------
21.48 store_pbt
21.49 - (prep_pbt (theory "Test")
21.50 - (["(theory "Test")"],
21.51 + (prep_pbt thy
21.52 + (["thy"],
21.53 [("#Given" ,"boolTestGiven g_"),
21.54 ("#Find" ,"boolTestFind f_")
21.55 ],
21.56 []));
21.57
21.58 store_pbt
21.59 - (prep_pbt (theory "Test")
21.60 - (["testeq","(theory "Test")"],
21.61 + (prep_pbt thy
21.62 + (["testeq","thy"],
21.63 [("#Given" ,"boolTestGiven g_"),
21.64 ("#Find" ,"boolTestFind f_")
21.65 ],
21.66 @@ -582,7 +584,7 @@
21.67 asm_rls=[],asm_thm=[]},
21.68 "Undef"));*)
21.69 store_met
21.70 - (prep_met (theory "Test") "met_test_solvelin" [] e_metID
21.71 + (prep_met thy "met_test_solvelin" [] e_metID
21.72 (["Test","solve_linear"]:metID,
21.73 [("#Given" ,["equality e_","solveFor v_"]),
21.74 ("#Where" ,["matches (?a = ?b) e_"]),
21.75 @@ -599,7 +601,7 @@
21.76 " (Rewrite_Set Test_simplify False))) e_" ^
21.77 " in [e_::bool])"
21.78 )
21.79 -(*, prep_met (theory "Test") (*test for equations*)
21.80 +(*, prep_met thy (*test for equations*)
21.81 (["Test","testeq"]:metID,
21.82 [("#Given" ,["boolTestGiven g_"]),
21.83 ("#Find" ,["boolTestFind f_"])
21.84 @@ -767,7 +769,7 @@
21.85 (** problem types **)
21.86
21.87 store_pbt
21.88 - (prep_pbt (theory "Test") "pbl_test_uni_plain2" [] e_pblID
21.89 + (prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
21.90 (["plain_square","univariate","equation","test"],
21.91 [("#Given" ,["equality e_","solveFor v_"]),
21.92 ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |" ^
21.93 @@ -802,7 +804,7 @@
21.94 *)
21.95
21.96 store_pbt
21.97 - (prep_pbt (theory "Test") "pbl_test_uni_poly" [] e_pblID
21.98 + (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
21.99 (["polynomial","univariate","equation","test"],
21.100 [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
21.101 ("#Where" ,["False"]),
21.102 @@ -811,7 +813,7 @@
21.103 e_rls, SOME "solve (e_::bool, v_)", []));
21.104
21.105 store_pbt
21.106 - (prep_pbt (theory "Test") "pbl_test_uni_poly_deg2" [] e_pblID
21.107 + (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
21.108 (["degree_two","polynomial","univariate","equation","test"],
21.109 [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
21.110 ("#Find" ,["solutions v_i_"])
21.111 @@ -819,7 +821,7 @@
21.112 e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
21.113
21.114 store_pbt
21.115 - (prep_pbt (theory "Test") "pbl_test_uni_poly_deg2_pq" [] e_pblID
21.116 + (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
21.117 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
21.118 [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),
21.119 ("#Find" ,["solutions v_i_"])
21.120 @@ -827,7 +829,7 @@
21.121 e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));
21.122
21.123 store_pbt
21.124 - (prep_pbt (theory "Test") "pbl_test_uni_poly_deg2_abc" [] e_pblID
21.125 + (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
21.126 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
21.127 [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_"]),
21.128 ("#Find" ,["solutions v_i_"])
21.129 @@ -835,7 +837,7 @@
21.130 e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_)", []));
21.131
21.132 store_pbt
21.133 - (prep_pbt (theory "Test") "pbl_test_uni_root" [] e_pblID
21.134 + (prep_pbt thy "pbl_test_uni_root" [] e_pblID
21.135 (["squareroot","univariate","equation","test"],
21.136 [("#Given" ,["equality e_","solveFor v_"]),
21.137 ("#Where" ,["contains_root (e_::bool)"]),
21.138 @@ -846,7 +848,7 @@
21.139 SOME "solve (e_::bool, v_)", [["Test","square_equation"]]));
21.140
21.141 store_pbt
21.142 - (prep_pbt (theory "Test") "pbl_test_uni_norm" [] e_pblID
21.143 + (prep_pbt thy "pbl_test_uni_norm" [] e_pblID
21.144 (["normalize","univariate","equation","test"],
21.145 [("#Given" ,["equality e_","solveFor v_"]),
21.146 ("#Where" ,[]),
21.147 @@ -855,7 +857,7 @@
21.148 e_rls, SOME "solve (e_::bool, v_)", [["Test","norm_univar_equation"]]));
21.149
21.150 store_pbt
21.151 - (prep_pbt (theory "Test") "pbl_test_uni_roottest" [] e_pblID
21.152 + (prep_pbt thy "pbl_test_uni_roottest" [] e_pblID
21.153 (["sqroot-test","univariate","equation","test"],
21.154 [("#Given" ,["equality e_","solveFor v_"]),
21.155 (*("#Where" ,["contains_root (e_::bool)"]),*)
21.156 @@ -869,7 +871,7 @@
21.157
21.158
21.159 store_met
21.160 - (prep_met (theory "Test") "met_test_sqrt" [] e_metID
21.161 + (prep_met thy "met_test_sqrt" [] e_metID
21.162 (*root-equation, version for tests before 8.01.01*)
21.163 (["Test","sqrt-equ-test"]:metID,
21.164 [("#Given" ,["equality e_","solveFor v_"]),
21.165 @@ -902,7 +904,7 @@
21.166 ));
21.167
21.168 store_met
21.169 - (prep_met (theory "Test") "met_test_sqrt2" [] e_metID
21.170 + (prep_met thy "met_test_sqrt2" [] e_metID
21.171 (*root-equation ... for test-*.sml until 8.01*)
21.172 (["Test","squ-equ-test2"]:metID,
21.173 [("#Given" ,["equality e_","solveFor v_"]),
21.174 @@ -934,7 +936,7 @@
21.175 ));
21.176
21.177 store_met
21.178 - (prep_met (theory "Test") "met_test_squ_sub" [] e_metID
21.179 + (prep_met thy "met_test_squ_sub" [] e_metID
21.180 (*tests subproblem fixed linear*)
21.181 (["Test","squ-equ-test-subpbl1"]:metID,
21.182 [("#Given" ,["equality e_","solveFor v_"]),
21.183 @@ -951,7 +953,7 @@
21.184 ));
21.185
21.186 store_met
21.187 - (prep_met (theory "Test") "met_test_squ_sub2" [] e_metID
21.188 + (prep_met thy "met_test_squ_sub2" [] e_metID
21.189 (*tests subproblem fixed degree 2*)
21.190 (["Test","squ-equ-test-subpbl2"]:metID,
21.191 [("#Given" ,["equality e_","solveFor v_"]),
21.192 @@ -969,7 +971,7 @@
21.193 ));
21.194
21.195 store_met
21.196 - (prep_met (theory "Test") "met_test_squ_nonterm" [] e_metID
21.197 + (prep_met thy "met_test_squ_nonterm" [] e_metID
21.198 (*root-equation: see foils..., but notTerminating*)
21.199 (["Test","square_equation...notTerminating"]:metID,
21.200 [("#Given" ,["equality e_","solveFor v_"]),
21.201 @@ -1000,7 +1002,7 @@
21.202 ));
21.203
21.204 store_met
21.205 - (prep_met (theory "Test") "met_test_eq1" [] e_metID
21.206 + (prep_met thy "met_test_eq1" [] e_metID
21.207 (*root-equation1:*)
21.208 (["Test","square_equation1"]:metID,
21.209 [("#Given" ,["equality e_","solveFor v_"]),
21.210 @@ -1030,7 +1032,7 @@
21.211 ));
21.212
21.213 store_met
21.214 - (prep_met (theory "Test") "met_test_squ2" [] e_metID
21.215 + (prep_met thy "met_test_squ2" [] e_metID
21.216 (*root-equation2*)
21.217 (["Test","square_equation2"]:metID,
21.218 [("#Given" ,["equality e_","solveFor v_"]),
21.219 @@ -1061,7 +1063,7 @@
21.220 ));
21.221
21.222 store_met
21.223 - (prep_met (theory "Test") "met_test_squeq" [] e_metID
21.224 + (prep_met thy "met_test_squeq" [] e_metID
21.225 (*root-equation*)
21.226 (["Test","square_equation"]:metID,
21.227 [("#Given" ,["equality e_","solveFor v_"]),
21.228 @@ -1092,7 +1094,7 @@
21.229 ) ); (*#######*)
21.230
21.231 store_met
21.232 - (prep_met (theory "Test") "met_test_eq_plain" [] e_metID
21.233 + (prep_met thy "met_test_eq_plain" [] e_metID
21.234 (*solve_plain_square*)
21.235 (["Test","solve_plain_square"]:metID,
21.236 [("#Given",["equality e_","solveFor v_"]),
21.237 @@ -1116,7 +1118,7 @@
21.238 ));
21.239
21.240 store_met
21.241 - (prep_met (theory "Test") "met_test_norm_univ" [] e_metID
21.242 + (prep_met thy "met_test_norm_univ" [] e_metID
21.243 (["Test","norm_univar_equation"]:metID,
21.244 [("#Given",["equality e_","solveFor v_"]),
21.245 ("#Where" ,[]),
22.1 --- a/src/Tools/isac/Knowledge/Vect.thy Wed Sep 01 16:15:13 2010 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Vect.thy Wed Sep 01 16:43:58 2010 +0200
22.3 @@ -1,5 +1,3 @@
22.4 Vect = Real +
22.5 -(*-------------------- consts ------------------------------------------------*)
22.6
22.7 -(*-------------------- rules -------------------------------------------------*)
22.8 end