1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Sep 06 14:48:38 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Sep 06 15:09:37 2010 +0200
     1.3 @@ -136,12 +136,12 @@
     1.4  store_pbt
     1.5   (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
     1.6   (["rat","sq","root","univariate","equation"],
     1.7 -  [("#Given" ,["equality e_","solveFor v_"]),
     1.8 -   ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) )| " ^
     1.9 -	       "( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]),
    1.10 -   ("#Find"  ,["solutions v_i_"])
    1.11 +  [("#Given" ,["equality e_e","solveFor v_v"]),
    1.12 +   ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_::real) )| " ^
    1.13 +	       "( (rhs e_e) is_rootRatAddTerm_in (v_::real) )"]),
    1.14 +   ("#Find"  ,["solutions v_i"])
    1.15     ],
    1.16 -  RootRatEq_prls, SOME "solve (e_::bool, v_)",
    1.17 +  RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
    1.18    [["RootRatEq","elim_rootrat_equation"]]));
    1.19  
    1.20  (*-------------------------Methode-----------------------*)
    1.21 @@ -155,10 +155,10 @@
    1.22  store_met
    1.23   (prep_met thy "met_rootrateq_elim" [] e_metID
    1.24   (["RootRatEq","elim_rootrat_equation"],
    1.25 -   [("#Given" ,["equality e_","solveFor v_"]),
    1.26 -    ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) ) | " ^
    1.27 -	       "( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]),
    1.28 -    ("#Find"  ,["solutions v_i_"])
    1.29 +   [("#Given" ,["equality e_e","solveFor v_v"]),
    1.30 +    ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_::real) ) | " ^
    1.31 +	       "( (rhs e_e) is_rootRatAddTerm_in (v_::real) )"]),
    1.32 +    ("#Find"  ,["solutions v_i"])
    1.33     ],
    1.34     {rew_ord'="termlessI",
    1.35      rls'=RooRatEq_erls,
    1.36 @@ -168,15 +168,15 @@
    1.37      crls=RootRatEq_crls, nrls=norm_Rational(*,
    1.38      asm_rls=[],
    1.39      asm_thm=[]*)},
    1.40 -   "Script Elim_rootrat_equation  (e_::bool) (v_::real)  =      " ^
    1.41 -    "(let e_ = ((Try (Rewrite_Set expand_rootbinoms False)) @@  " ^ 
    1.42 +   "Script Elim_rootrat_equation  (e_e::bool) (v_::real)  =      " ^
    1.43 +    "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@  " ^ 
    1.44      "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^ 
    1.45      "           (Try (Rewrite_Set make_rooteq       False)) @@  " ^
    1.46      "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^
    1.47      "           (Try (Rewrite_Set_Inst [(bdv,v_)]               " ^
    1.48 -    "                                  rootrat_solve False))) e_ " ^
    1.49 +    "                                  rootrat_solve False))) e_e " ^
    1.50      " in (SubProblem (RootEq_,[univariate,equation],            " ^
    1.51 -    "        [no_met]) [bool_ e_, real_ v_]))"
    1.52 +    "        [no_met]) [bool_ e_e, real_ v_]))"
    1.53     ));
    1.54  calclist':= overwritel (!calclist', 
    1.55     [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",