1.1 --- a/src/Tools/isac/Knowledge/Equation.thy Fri Aug 27 10:28:44 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Fri Aug 27 10:39:12 2010 +0200
1.3 @@ -38,7 +38,7 @@
1.4
1.5
1.6 store_pbt
1.7 - (prep_pbt Equation.thy "pbl_equ" [] e_pblID
1.8 + (prep_pbt (theory "Equation") "pbl_equ" [] e_pblID
1.9 (["equation"],
1.10 [("#Given" ,["equality e_","solveFor v_"]),
1.11 ("#Where" ,["matches (?a = ?b) e_"]),
1.12 @@ -50,7 +50,7 @@
1.13 []));
1.14
1.15 store_pbt
1.16 - (prep_pbt Equation.thy "pbl_equ_univ" [] e_pblID
1.17 + (prep_pbt (theory "Equation") "pbl_equ_univ" [] e_pblID
1.18 (["univariate","equation"],
1.19 [("#Given" ,["equality e_","solveFor v_"]),
1.20 ("#Where" ,["matches (?a = ?b) e_"]),
1.21 @@ -86,7 +86,7 @@
1.22
1.23
1.24 store_met
1.25 - (prep_met Equation.thy "met_equ" [] e_metID
1.26 + (prep_met (theory "Equation") "met_equ" [] e_metID
1.27 (["Equation"],
1.28 [],
1.29 {rew_ord'="tless_true", rls'=Erls, calc = [],
2.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Fri Aug 27 10:28:44 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Fri Aug 27 10:39:12 2010 +0200
2.3 @@ -124,7 +124,7 @@
2.4 *)
2.5 (* ---------linear----------- *)
2.6 store_pbt
2.7 - (prep_pbt LinEq.thy "pbl_equ_univ_lin" [] e_pblID
2.8 + (prep_pbt (theory "LinEq") "pbl_equ_univ_lin" [] e_pblID
2.9 (["linear","univariate","equation"],
2.10 [("#Given" ,["equality e_","solveFor v_"]),
2.11 ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*)
2.12 @@ -139,7 +139,7 @@
2.13
2.14 (*-------------- methods------------------------------------------------------*)
2.15 store_met
2.16 - (prep_met LinEq.thy "met_eqlin" [] e_metID
2.17 + (prep_met (theory "LinEq") "met_eqlin" [] e_metID
2.18 (["LinEq"],
2.19 [],
2.20 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
2.21 @@ -148,7 +148,7 @@
2.22
2.23 (* ansprechen mit ["LinEq","solve_univar_equation"] *)
2.24 store_met
2.25 -(prep_met LinEq.thy "met_eq_lin" [] e_metID
2.26 +(prep_met (theory "LinEq") "met_eq_lin" [] e_metID
2.27 (["LinEq","solve_lineq_equation"],
2.28 [("#Given" ,["equality e_","solveFor v_"]),
2.29 ("#Where" ,["Not( (lhs e_) is_polyrat_in v_)",
3.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Aug 27 10:28:44 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Aug 27 10:39:12 2010 +0200
3.3 @@ -833,7 +833,7 @@
3.4 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
3.5 val order_add_mult =
3.6 Rls{id = "order_add_mult", preconds = [],
3.7 - rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy),
3.8 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false (theory "Poly")),
3.9 erls = e_rls,srls = Erls,
3.10 calc = [],
3.11 (*asm_thm = [],*)
3.12 @@ -854,7 +854,7 @@
3.13 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
3.14 val order_mult =
3.15 Rls{id = "order_mult", preconds = [],
3.16 - rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy),
3.17 + rew_ord = ("ord_make_polynomial",ord_make_polynomial false (theory "Poly")),
3.18 erls = e_rls,srls = Erls,
3.19 calc = [],
3.20 (*asm_thm = [],*)
3.21 @@ -1383,7 +1383,7 @@
3.22 rew_ord = ("dummy_ord", dummy_ord),
3.23 erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*)
3.24 [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")
3.25 - (*WN.18.6.03 definiert in Poly.thy,
3.26 + (*WN.18.6.03 definiert in (theory "Poly"),
3.27 evaluiert prepat*)],
3.28 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
3.29 ("TIMES" ,("op *" ,eval_binop "#mult_")),
3.30 @@ -1579,7 +1579,7 @@
3.31 (** problems **)
3.32
3.33 store_pbt
3.34 - (prep_pbt Poly.thy "pbl_simp_poly" [] e_pblID
3.35 + (prep_pbt (theory "Poly") "pbl_simp_poly" [] e_pblID
3.36 (["polynomial","simplification"],
3.37 [("#Given" ,["term t_"]),
3.38 ("#Where" ,["t_ is_polyexp"]),
3.39 @@ -1594,7 +1594,7 @@
3.40 (** methods **)
3.41
3.42 store_met
3.43 - (prep_met Poly.thy "met_simp_poly" [] e_metID
3.44 + (prep_met (theory "Poly") "met_simp_poly" [] e_metID
3.45 (["simplification","for_polynomials"],
3.46 [("#Given" ,["term t_"]),
3.47 ("#Where" ,["t_ is_polyexp"]),
4.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Fri Aug 27 10:28:44 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Fri Aug 27 10:39:12 2010 +0200
4.3 @@ -397,12 +397,12 @@
4.4 (** problems **)
4.5
4.6 store_pbt
4.7 - (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID
4.8 + (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly" [] e_pblID
4.9 (["polynom","vereinfachen"],
4.10 [], Erls, NONE, []));
4.11
4.12 store_pbt
4.13 - (prep_pbt PolyMinus.thy "pbl_vereinf_poly_minus" [] e_pblID
4.14 + (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_minus" [] e_pblID
4.15 (["plus_minus","polynom","vereinfachen"],
4.16 [("#Given" ,["term t_"]),
4.17 ("#Where" ,["t_ is_polyexp",
4.18 @@ -431,7 +431,7 @@
4.19 [["simplification","for_polynomials","with_minus"]]));
4.20
4.21 store_pbt
4.22 - (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer" [] e_pblID
4.23 + (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_klammer" [] e_pblID
4.24 (["klammer","polynom","vereinfachen"],
4.25 [("#Given" ,["term t_"]),
4.26 ("#Where" ,["t_ is_polyexp",
4.27 @@ -455,7 +455,7 @@
4.28 [["simplification","for_polynomials","with_parentheses"]]));
4.29
4.30 store_pbt
4.31 - (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
4.32 + (prep_pbt (theory "PolyMinus") "pbl_vereinf_poly_klammer_mal" [] e_pblID
4.33 (["binom_klammer","polynom","vereinfachen"],
4.34 [("#Given" ,["term t_"]),
4.35 ("#Where" ,["t_ is_polyexp"]),
4.36 @@ -467,12 +467,12 @@
4.37 [["simplification","for_polynomials","with_parentheses_mult"]]));
4.38
4.39 store_pbt
4.40 - (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID
4.41 + (prep_pbt (theory "PolyMinus") "pbl_probe" [] e_pblID
4.42 (["probe"],
4.43 [], Erls, NONE, []));
4.44
4.45 store_pbt
4.46 - (prep_pbt PolyMinus.thy "pbl_probe_poly" [] e_pblID
4.47 + (prep_pbt (theory "PolyMinus") "pbl_probe_poly" [] e_pblID
4.48 (["polynom","probe"],
4.49 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
4.50 ("#Where" ,["e_ is_polyexp"]),
4.51 @@ -485,7 +485,7 @@
4.52 [["probe","fuer_polynom"]]));
4.53
4.54 store_pbt
4.55 - (prep_pbt PolyMinus.thy "pbl_probe_bruch" [] e_pblID
4.56 + (prep_pbt (theory "PolyMinus") "pbl_probe_bruch" [] e_pblID
4.57 (["bruch","probe"],
4.58 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
4.59 ("#Where" ,["e_ is_ratpolyexp"]),
4.60 @@ -501,7 +501,7 @@
4.61 (** methods **)
4.62
4.63 store_met
4.64 - (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID
4.65 + (prep_met (theory "PolyMinus") "met_simp_poly_minus" [] e_metID
4.66 (["simplification","for_polynomials","with_minus"],
4.67 [("#Given" ,["term t_"]),
4.68 ("#Where" ,["t_ is_polyexp",
4.69 @@ -531,7 +531,7 @@
4.70 ));
4.71
4.72 store_met
4.73 - (prep_met PolyMinus.thy "met_simp_poly_parenth" [] e_metID
4.74 + (prep_met (theory "PolyMinus") "met_simp_poly_parenth" [] e_metID
4.75 (["simplification","for_polynomials","with_parentheses"],
4.76 [("#Given" ,["term t_"]),
4.77 ("#Where" ,["t_ is_polyexp"]),
4.78 @@ -550,7 +550,7 @@
4.79 ));
4.80
4.81 store_met
4.82 - (prep_met PolyMinus.thy "met_simp_poly_parenth_mult" [] e_metID
4.83 + (prep_met (theory "PolyMinus") "met_simp_poly_parenth_mult" [] e_metID
4.84 (["simplification","for_polynomials","with_parentheses_mult"],
4.85 [("#Given" ,["term t_"]),
4.86 ("#Where" ,["t_ is_polyexp"]),
4.87 @@ -572,7 +572,7 @@
4.88 ));
4.89
4.90 store_met
4.91 - (prep_met PolyMinus.thy "met_probe" [] e_metID
4.92 + (prep_met (theory "PolyMinus") "met_probe" [] e_metID
4.93 (["probe"],
4.94 [],
4.95 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
4.96 @@ -580,7 +580,7 @@
4.97 "empty_script"));
4.98
4.99 store_met
4.100 - (prep_met PolyMinus.thy "met_probe_poly" [] e_metID
4.101 + (prep_met (theory "PolyMinus") "met_probe_poly" [] e_metID
4.102 (["probe","fuer_polynom"],
4.103 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
4.104 ("#Where" ,["e_ is_polyexp"]),
4.105 @@ -601,7 +601,7 @@
4.106 ));
4.107
4.108 store_met
4.109 - (prep_met PolyMinus.thy "met_probe_bruch" [] e_metID
4.110 + (prep_met (theory "PolyMinus") "met_probe_bruch" [] e_metID
4.111 (["probe","fuer_bruch"],
4.112 [("#Given" ,["Pruefe e_", "mitWert ws_"]),
4.113 ("#Where" ,["e_ is_ratpolyexp"]),
5.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Aug 27 10:28:44 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Aug 27 10:39:12 2010 +0200
5.3 @@ -2886,7 +2886,7 @@
5.4 val {rules, rew_ord=(_,ro),...} =
5.5 rep_rls (assoc_rls "rev_rew_p");
5.6
5.7 -val thy = Rational.thy;
5.8 +val thy = (theory "Rational");
5.9
5.10 (*.init_state = fn : term -> istate
5.11 initialzies the state of the script interpreter. The state is:
5.12 @@ -2904,7 +2904,7 @@
5.13 (#) could be extracted from here by (map #1)*).*)
5.14 (* val {rules, rew_ord=(_,ro),...} =
5.15 rep_rls (assoc_rls "rev_rew_p") (*USE ALWAYS, SEE val cancel_p*);
5.16 - val (thy, eval_rls, ro) =(Rational.thy, Atools_erls, ro) (*..val cancel_p*);
5.17 + val (thy, eval_rls, ro) =((theory "Rational"), Atools_erls, ro) (*..val cancel_p*);
5.18 val t = t;
5.19 *)
5.20 fun init_state thy eval_rls ro t =
5.21 @@ -2961,12 +2961,12 @@
5.22 value:
5.23 -> rule option: ... this rule is appropriate for cancellation;
5.24 there may be no such rule (if the term is canceled already.*)
5.25 -(* val thy = Rational.thy;
5.26 +(* val thy = (theory "Rational");
5.27 val Rrls {rew_ord=(_,ro),...} = cancel;
5.28 val ([rs],t) = (rss,f);
5.29 next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)
5.30
5.31 - val (thy, [rs]) = (Rational.thy, revsets);
5.32 + val (thy, [rs]) = ((theory "Rational"), revsets);
5.33 val Rrls {rew_ord=(_,ro),...} = cancel;
5.34 nex [rs] t;
5.35 *)
5.36 @@ -3003,7 +3003,7 @@
5.37 val cancel_p =
5.38 Rrls {id = "cancel_p", prepat=[],
5.39 rew_ord=("ord_make_polynomial",
5.40 - ord_make_polynomial false Rational.thy),
5.41 + ord_make_polynomial false (theory "Rational")),
5.42 erls = rational_erls,
5.43 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
5.44 ("TIMES" ,("op *" ,eval_binop "#mult_")),
5.45 @@ -3036,7 +3036,7 @@
5.46 *)
5.47 val {rules=rules,rew_ord=(_,ro),...} =
5.48 rep_rls (assoc_rls "expand_binoms");
5.49 -val thy = Rational.thy;
5.50 +val thy = (theory "Rational");
5.51
5.52 fun init_state thy eval_rls ro t =
5.53 let val SOME (t',_) = factout_ thy t;
5.54 @@ -3086,7 +3086,7 @@
5.55 val cancel =
5.56 Rrls {id = "cancel", prepat=prepat,
5.57 rew_ord=("ord_make_polynomial",
5.58 - ord_make_polynomial false Rational.thy),
5.59 + ord_make_polynomial false (theory "Rational")),
5.60 erls = rational_erls,
5.61 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
5.62 ("TIMES" ,("op *" ,eval_binop "#mult_")),
5.63 @@ -3112,7 +3112,7 @@
5.64 see rational.sml --- investigate rulesets for cancel_p ---*)
5.65 val {rules, rew_ord=(_,ro),...} =
5.66 rep_rls (assoc_rls "rev_rew_p");
5.67 -val thy = Rational.thy;
5.68 +val thy = (theory "Rational");
5.69
5.70
5.71 (*.common_nominator_p_ = fn : theory -> term -> (term * term list) option
5.72 @@ -3188,12 +3188,12 @@
5.73 value:
5.74 -> rule option: ... this rule is appropriate for cancellation;
5.75 there may be no such rule (if the term is canceled already.*)
5.76 -(* val thy = Rational.thy;
5.77 +(* val thy = (theory "Rational");
5.78 val Rrls {rew_ord=(_,ro),...} = cancel;
5.79 val ([rs],t) = (rss,f);
5.80 next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)
5.81
5.82 - val (thy, [rs]) = (Rational.thy, revsets);
5.83 + val (thy, [rs]) = ((theory "Rational"), revsets);
5.84 val Rrls {rew_ord=(_,ro),...} = cancel;
5.85 nex [rs] t;
5.86 *)
5.87 @@ -3240,7 +3240,7 @@
5.88 val common_nominator_p =
5.89 Rrls {id = "common_nominator_p", prepat=prepat,
5.90 rew_ord=("ord_make_polynomial",
5.91 - ord_make_polynomial false Rational.thy),
5.92 + ord_make_polynomial false (theory "Rational")),
5.93 erls = rational_erls,
5.94 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
5.95 ("TIMES" ,("op *" ,eval_binop "#mult_")),
5.96 @@ -3261,7 +3261,7 @@
5.97
5.98 val {rules=rules,rew_ord=(_,ro),...} =
5.99 rep_rls (assoc_rls "make_polynomial");
5.100 -val thy = Rational.thy;
5.101 +val thy = (theory "Rational");
5.102
5.103
5.104 (*.common_nominator_ = fn : theory -> term -> (term * term list) option
5.105 @@ -3337,12 +3337,12 @@
5.106 value:
5.107 -> rule option: ... this rule is appropriate for cancellation;
5.108 there may be no such rule (if the term is canceled already.*)
5.109 -(* val thy = Rational.thy;
5.110 +(* val thy = (theory "Rational");
5.111 val Rrls {rew_ord=(_,ro),...} = cancel;
5.112 val ([rs],t) = (rss,f);
5.113 next_rule thy eval_rls ro [rs] t;(*eval fun next_rule ... before!*)
5.114
5.115 - val (thy, [rs]) = (Rational.thy, revsets);
5.116 + val (thy, [rs]) = ((theory "Rational"), revsets);
5.117 val Rrls {rew_ord=(_,ro),...} = cancel_p;
5.118 nex [rs] t;
5.119 *)
5.120 @@ -3393,7 +3393,7 @@
5.121 val common_nominator =
5.122 Rrls {id = "common_nominator", prepat=prepat,
5.123 rew_ord=("ord_make_polynomial",
5.124 - ord_make_polynomial false Rational.thy),
5.125 + ord_make_polynomial false (theory "Rational")),
5.126 erls = rational_erls,
5.127 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
5.128 ("TIMES" ,("op *" ,eval_binop "#mult_")),
5.129 @@ -3611,10 +3611,6 @@
5.130 (*-------------------18.3.03 --> struct <-----------^^^--*)
5.131
5.132
5.133 -
5.134 -theory' := overwritel (!theory', [("Rational.thy",Rational.thy)]);
5.135 -
5.136 -
5.137 (*WN030318???SK: simplifies all but cancel and common_nominator*)
5.138 val simplify_rational =
5.139 merge_rls "simplify_rational" expand_binoms
5.140 @@ -3796,7 +3792,7 @@
5.141 (** problems **)
5.142
5.143 store_pbt
5.144 - (prep_pbt Rational.thy "pbl_simp_rat" [] e_pblID
5.145 + (prep_pbt (theory "Rational") "pbl_simp_rat" [] e_pblID
5.146 (["rational","simplification"],
5.147 [("#Given" ,["term t_"]),
5.148 ("#Where" ,["t_ is_ratpolyexp"]),
5.149 @@ -3811,7 +3807,7 @@
5.150 (*WN061025 this methods script is copied from (auto-generated) script
5.151 of norm_Rational in order to ease repair on inform*)
5.152 store_met
5.153 - (prep_met Rational.thy "met_simp_rat" [] e_metID
5.154 + (prep_met (theory "Rational") "met_simp_rat" [] e_metID
5.155 (["simplification","of_rationals"],
5.156 [("#Given" ,["term t_"]),
5.157 ("#Where" ,["t_ is_ratpolyexp"]),
6.1 --- a/src/Tools/isac/Knowledge/Root.thy Fri Aug 27 10:28:44 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Root.thy Fri Aug 27 10:39:12 2010 +0200
6.3 @@ -191,7 +191,7 @@
6.4
6.5 val make_rooteq = prep_rls(
6.6 Rls{id = "make_rooteq", preconds = []:term list,
6.7 - rew_ord = ("sqrt_right", sqrt_right false Root.thy),
6.8 + rew_ord = ("sqrt_right", sqrt_right false (theory "Root")),
6.9 erls = Atools_erls, srls = Erls,
6.10 calc = [],
6.11 (*asm_thm = [],*)
7.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Fri Aug 27 10:28:44 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Fri Aug 27 10:39:12 2010 +0200
7.3 @@ -475,7 +475,7 @@
7.4 *)
7.5 (* ---------root----------- *)
7.6 store_pbt
7.7 - (prep_pbt RootEq.thy "pbl_equ_univ_root" [] e_pblID
7.8 + (prep_pbt (theory "RootEq") "pbl_equ_univ_root" [] e_pblID
7.9 (["root","univariate","equation"],
7.10 [("#Given" ,["equality e_","solveFor v_"]),
7.11 ("#Where" ,["(lhs e_) is_rootTerm_in (v_::real) | " ^
7.12 @@ -486,7 +486,7 @@
7.13 []));
7.14 (* ---------sqrt----------- *)
7.15 store_pbt
7.16 - (prep_pbt RootEq.thy "pbl_equ_univ_root_sq" [] e_pblID
7.17 + (prep_pbt (theory "RootEq") "pbl_equ_univ_root_sq" [] e_pblID
7.18 (["sq","root","univariate","equation"],
7.19 [("#Given" ,["equality e_","solveFor v_"]),
7.20 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
7.21 @@ -499,7 +499,7 @@
7.22 [["RootEq","solve_sq_root_equation"]]));
7.23 (* ---------normalize----------- *)
7.24 store_pbt
7.25 - (prep_pbt RootEq.thy "pbl_equ_univ_root_norm" [] e_pblID
7.26 + (prep_pbt (theory "RootEq") "pbl_equ_univ_root_norm" [] e_pblID
7.27 (["normalize","root","univariate","equation"],
7.28 [("#Given" ,["equality e_","solveFor v_"]),
7.29 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
7.30 @@ -514,7 +514,7 @@
7.31 (*-------------------------methods-----------------------*)
7.32 (* ---- root 20.8.02 ---*)
7.33 store_met
7.34 - (prep_met RootEq.thy "met_rooteq" [] e_metID
7.35 + (prep_met (theory "RootEq") "met_rooteq" [] e_metID
7.36 (["RootEq"],
7.37 [],
7.38 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
7.39 @@ -522,7 +522,7 @@
7.40 asm_rls=[],asm_thm=[]*)}, "empty_script"));
7.41 (*-- normalize 20.10.02 --*)
7.42 store_met
7.43 - (prep_met RootEq.thy "met_rooteq_norm" [] e_metID
7.44 + (prep_met (theory "RootEq") "met_rooteq_norm" [] e_metID
7.45 (["RootEq","norm_sq_root_equation"],
7.46 [("#Given" ,["equality e_","solveFor v_"]),
7.47 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
7.48 @@ -550,7 +550,7 @@
7.49 ));
7.50
7.51 store_met
7.52 - (prep_met RootEq.thy "met_rooteq_sq" [] e_metID
7.53 + (prep_met (theory "RootEq") "met_rooteq_sq" [] e_metID
7.54 (["RootEq","solve_sq_root_equation"],
7.55 [("#Given" ,["equality e_","solveFor v_"]),
7.56 ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
7.57 @@ -583,7 +583,7 @@
7.58
7.59 (*-- right 28.08.02 --*)
7.60 store_met
7.61 - (prep_met RootEq.thy "met_rooteq_sq_right" [] e_metID
7.62 + (prep_met (theory "RootEq") "met_rooteq_sq_right" [] e_metID
7.63 (["RootEq","solve_right_sq_root_equation"],
7.64 [("#Given" ,["equality e_","solveFor v_"]),
7.65 ("#Where" ,["(rhs e_) is_sqrtTerm_in v_"]),
7.66 @@ -611,7 +611,7 @@
7.67
7.68 (*-- left 28.08.02 --*)
7.69 store_met
7.70 - (prep_met RootEq.thy "met_rooteq_sq_left" [] e_metID
7.71 + (prep_met (theory "RootEq") "met_rooteq_sq_left" [] e_metID
7.72 (["RootEq","solve_left_sq_root_equation"],
7.73 [("#Given" ,["equality e_","solveFor v_"]),
7.74 ("#Where" ,["(lhs e_) is_sqrtTerm_in v_"]),
8.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Fri Aug 27 10:28:44 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Fri Aug 27 10:39:12 2010 +0200
8.3 @@ -29,7 +29,7 @@
8.4
8.5 (** problems **)
8.6 store_pbt
8.7 - (prep_pbt Simplify.thy "pbl_simp" [] e_pblID
8.8 + (prep_pbt (theory "Simplify") "pbl_simp" [] e_pblID
8.9 (["simplification"],
8.10 [("#Given" ,["term t_"]),
8.11 ("#Find" ,["normalform n_"])
8.12 @@ -39,7 +39,7 @@
8.13 []));
8.14
8.15 store_pbt
8.16 - (prep_pbt Simplify.thy "pbl_vereinfache" [] e_pblID
8.17 + (prep_pbt (theory "Simplify") "pbl_vereinfache" [] e_pblID
8.18 (["vereinfachen"],
8.19 [("#Given" ,["term t_"]),
8.20 ("#Find" ,["normalform n_"])
8.21 @@ -51,7 +51,7 @@
8.22 (** methods **)
8.23
8.24 store_met
8.25 - (prep_met Simplify.thy "met_simp" [] e_metID
8.26 + (prep_met (theory "Simplify") "met_simp" [] e_metID
8.27 (["simplification"],
8.28 [("#Given" ,["term t_"]),
8.29 ("#Find" ,["normalform n_"])