1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Fri Aug 27 10:28:44 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Fri Aug 27 10:39:12 2010 +0200
     1.3 @@ -475,7 +475,7 @@
     1.4  *)
     1.5  (* ---------root----------- *)
     1.6  store_pbt
     1.7 - (prep_pbt RootEq.thy "pbl_equ_univ_root" [] e_pblID
     1.8 + (prep_pbt (theory "RootEq") "pbl_equ_univ_root" [] e_pblID
     1.9   (["root","univariate","equation"],
    1.10    [("#Given" ,["equality e_","solveFor v_"]),
    1.11     ("#Where" ,["(lhs e_) is_rootTerm_in  (v_::real) | " ^
    1.12 @@ -486,7 +486,7 @@
    1.13    []));
    1.14  (* ---------sqrt----------- *)
    1.15  store_pbt
    1.16 - (prep_pbt RootEq.thy "pbl_equ_univ_root_sq" [] e_pblID
    1.17 + (prep_pbt (theory "RootEq") "pbl_equ_univ_root_sq" [] e_pblID
    1.18   (["sq","root","univariate","equation"],
    1.19    [("#Given" ,["equality e_","solveFor v_"]),
    1.20     ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
    1.21 @@ -499,7 +499,7 @@
    1.22    [["RootEq","solve_sq_root_equation"]]));
    1.23  (* ---------normalize----------- *)
    1.24  store_pbt
    1.25 - (prep_pbt RootEq.thy "pbl_equ_univ_root_norm" [] e_pblID
    1.26 + (prep_pbt (theory "RootEq") "pbl_equ_univ_root_norm" [] e_pblID
    1.27   (["normalize","root","univariate","equation"],
    1.28    [("#Given" ,["equality e_","solveFor v_"]),
    1.29     ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
    1.30 @@ -514,7 +514,7 @@
    1.31  (*-------------------------methods-----------------------*)
    1.32  (* ---- root 20.8.02 ---*)
    1.33  store_met
    1.34 - (prep_met RootEq.thy "met_rooteq" [] e_metID
    1.35 + (prep_met (theory "RootEq") "met_rooteq" [] e_metID
    1.36   (["RootEq"],
    1.37     [],
    1.38     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
    1.39 @@ -522,7 +522,7 @@
    1.40      asm_rls=[],asm_thm=[]*)}, "empty_script"));
    1.41  (*-- normalize 20.10.02 --*)
    1.42  store_met
    1.43 - (prep_met RootEq.thy "met_rooteq_norm" [] e_metID
    1.44 + (prep_met (theory "RootEq") "met_rooteq_norm" [] e_metID
    1.45   (["RootEq","norm_sq_root_equation"],
    1.46     [("#Given" ,["equality e_","solveFor v_"]),
    1.47      ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
    1.48 @@ -550,7 +550,7 @@
    1.49     ));
    1.50  
    1.51  store_met
    1.52 - (prep_met RootEq.thy "met_rooteq_sq" [] e_metID
    1.53 + (prep_met (theory "RootEq") "met_rooteq_sq" [] e_metID
    1.54   (["RootEq","solve_sq_root_equation"],
    1.55     [("#Given" ,["equality e_","solveFor v_"]),
    1.56      ("#Where" ,["( ((lhs e_) is_sqrtTerm_in (v_::real)) &" ^
    1.57 @@ -583,7 +583,7 @@
    1.58  
    1.59  (*-- right 28.08.02 --*)
    1.60  store_met
    1.61 - (prep_met RootEq.thy "met_rooteq_sq_right" [] e_metID
    1.62 + (prep_met (theory "RootEq") "met_rooteq_sq_right" [] e_metID
    1.63   (["RootEq","solve_right_sq_root_equation"],
    1.64     [("#Given" ,["equality e_","solveFor v_"]),
    1.65      ("#Where" ,["(rhs e_) is_sqrtTerm_in v_"]),
    1.66 @@ -611,7 +611,7 @@
    1.67  
    1.68  (*-- left 28.08.02 --*)
    1.69  store_met
    1.70 - (prep_met RootEq.thy "met_rooteq_sq_left" [] e_metID
    1.71 + (prep_met (theory "RootEq") "met_rooteq_sq_left" [] e_metID
    1.72   (["RootEq","solve_left_sq_root_equation"],
    1.73     [("#Given" ,["equality e_","solveFor v_"]),
    1.74      ("#Where" ,["(lhs e_) is_sqrtTerm_in v_"]),