1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Mon Jan 27 21:58:57 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Mon Jan 27 22:26:51 2014 +0100
     1.3 @@ -485,45 +485,9 @@
     1.4  (get_pbt ["root'","univariate","equation"]);
     1.5  show_ptyps(); 
     1.6  *)
     1.7 -(* ---------root----------- *)
     1.8 -store_pbt
     1.9 - (prep_pbt thy "pbl_equ_univ_root" [] e_pblID
    1.10 - (["root'","univariate","equation"],
    1.11 -  [("#Given" ,["equality e_e","solveFor v_v"]),
    1.12 -   ("#Where" ,["(lhs e_e) is_rootTerm_in  (v_v::real) | " ^
    1.13 -	       "(rhs e_e) is_rootTerm_in  (v_v::real)"]),
    1.14 -   ("#Find"  ,["solutions v_v'i'"]) 
    1.15 -  ],
    1.16 -  RootEq_prls, SOME "solve (e_e::bool, v_v)",
    1.17 -  []));
    1.18 -(* ---------sqrt----------- *)
    1.19 -store_pbt
    1.20 - (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID
    1.21 - (["sq","root'","univariate","equation"],
    1.22 -  [("#Given" ,["equality e_e","solveFor v_v"]),
    1.23 -   ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
    1.24 -               "  ((lhs e_e) is_normSqrtTerm_in (v_v::real))   )  |" ^
    1.25 -	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
    1.26 -               "  ((rhs e_e) is_normSqrtTerm_in (v_v::real))   )"]),
    1.27 -   ("#Find"  ,["solutions v_v'i'"]) 
    1.28 -  ],
    1.29 -  RootEq_prls,  SOME "solve (e_e::bool, v_v)",
    1.30 -  [["RootEq","solve_sq_root_equation"]]));
    1.31 -(* ---------normalize----------- *)
    1.32 -store_pbt
    1.33 - (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID
    1.34 - (["normalize","root'","univariate","equation"],
    1.35 -  [("#Given" ,["equality e_e","solveFor v_v"]),
    1.36 -   ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
    1.37 -               "  Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  | " ^
    1.38 -	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
    1.39 -               "  Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
    1.40 -   ("#Find"  ,["solutions v_v'i'"]) 
    1.41 -  ],
    1.42 -  RootEq_prls,  SOME "solve (e_e::bool, v_v)",
    1.43 -  [["RootEq","norm_sq_root_equation"]]));
    1.44  *}
    1.45  setup {* KEStore_Elems.add_pbts
    1.46 +  (* ---------root----------- *)
    1.47    [(prep_pbt thy "pbl_equ_univ_root" [] e_pblID
    1.48        (["root'","univariate","equation"],
    1.49          [("#Given" ,["equality e_e","solveFor v_v"]),