1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Thu Sep 23 08:43:36 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Thu Sep 23 08:54:26 2010 +0200
     1.3 @@ -482,7 +482,7 @@
     1.4    [("#Given" ,["equality e_e","solveFor v_v"]),
     1.5     ("#Where" ,["(lhs e_e) is_rootTerm_in  (v_v::real) | " ^
     1.6  	       "(rhs e_e) is_rootTerm_in  (v_v::real)"]),
     1.7 -   ("#Find"  ,["solutions v'i'"]) 
     1.8 +   ("#Find"  ,["solutions v_v'i'"]) 
     1.9    ],
    1.10    RootEq_prls, SOME "solve (e_e::bool, v_v)",
    1.11    []));
    1.12 @@ -495,7 +495,7 @@
    1.13                 "  ((lhs e_e) is_normSqrtTerm_in (v_v::real))   )  |" ^
    1.14  	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
    1.15                 "  ((rhs e_e) is_normSqrtTerm_in (v_v::real))   )"]),
    1.16 -   ("#Find"  ,["solutions v'i'"]) 
    1.17 +   ("#Find"  ,["solutions v_v'i'"]) 
    1.18    ],
    1.19    RootEq_prls,  SOME "solve (e_e::bool, v_v)",
    1.20    [["RootEq","solve_sq_root_equation"]]));
    1.21 @@ -508,7 +508,7 @@
    1.22                 "  Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  | " ^
    1.23  	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
    1.24                 "  Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
    1.25 -   ("#Find"  ,["solutions v'i'"]) 
    1.26 +   ("#Find"  ,["solutions v_v'i'"]) 
    1.27    ],
    1.28    RootEq_prls,  SOME "solve (e_e::bool, v_v)",
    1.29    [["RootEq","norm_sq_root_equation"]]));
    1.30 @@ -532,7 +532,7 @@
    1.31                 "  Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  | " ^
    1.32  	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
    1.33                 "  Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
    1.34 -    ("#Find"  ,["solutions v'i'"])
    1.35 +    ("#Find"  ,["solutions v_v'i'"])
    1.36     ],
    1.37     {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
    1.38      calc=[], crls=RootEq_crls, nrls=norm_Poly},
    1.39 @@ -558,7 +558,7 @@
    1.40                  " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
    1.41  	        "(((rhs e_e) is_sqrtTerm_in (v_v::real))     & " ^
    1.42                  " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
    1.43 -    ("#Find"  ,["solutions v'i'"])
    1.44 +    ("#Find"  ,["solutions v_v'i'"])
    1.45     ],
    1.46     {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
    1.47      prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly},
    1.48 @@ -586,7 +586,7 @@
    1.49   (["RootEq","solve_right_sq_root_equation"],
    1.50     [("#Given" ,["equality e_e","solveFor v_v"]),
    1.51      ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
    1.52 -    ("#Find"  ,["solutions v'i'"])
    1.53 +    ("#Find"  ,["solutions v_v'i'"])
    1.54     ],
    1.55     {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, 
    1.56      prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly},
    1.57 @@ -611,7 +611,7 @@
    1.58   (["RootEq","solve_left_sq_root_equation"],
    1.59     [("#Given" ,["equality e_e","solveFor v_v"]),
    1.60      ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
    1.61 -    ("#Find"  ,["solutions v'i'"])
    1.62 +    ("#Find"  ,["solutions v_v'i'"])
    1.63     ],
    1.64     {rew_ord'="termlessI",
    1.65      rls'=RootEq_erls,