diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/RootEq.thy
--- a/src/Tools/isac/Knowledge/RootEq.thy	Tue Sep 14 12:12:42 2010 +0200
+++ b/src/Tools/isac/Knowledge/RootEq.thy	Tue Sep 14 15:46:56 2010 +0200
@@ -482,7 +482,7 @@
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(lhs e_e) is_rootTerm_in  (v_v::real) | " ^
 	       "(rhs e_e) is_rootTerm_in  (v_v::real)"]),
-   ("#Find"  ,["solutions v_i'''"]) 
+   ("#Find"  ,["solutions v'i'"]) 
   ],
   RootEq_prls, SOME "solve (e_e::bool, v_v)",
   []));
@@ -495,7 +495,7 @@
                "  ((lhs e_e) is_normSqrtTerm_in (v_v::real))   )  |" ^
 	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
                "  ((rhs e_e) is_normSqrtTerm_in (v_v::real))   )"]),
-   ("#Find"  ,["solutions v_i'''"]) 
+   ("#Find"  ,["solutions v'i'"]) 
   ],
   RootEq_prls,  SOME "solve (e_e::bool, v_v)",
   [["RootEq","solve_sq_root_equation"]]));
@@ -508,7 +508,7 @@
                "  Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  | " ^
 	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
                "  Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
-   ("#Find"  ,["solutions v_i'''"]) 
+   ("#Find"  ,["solutions v'i'"]) 
   ],
   RootEq_prls,  SOME "solve (e_e::bool, v_v)",
   [["RootEq","norm_sq_root_equation"]]));
@@ -532,7 +532,7 @@
                "  Not((lhs e_e) is_normSqrtTerm_in (v_v::real)))  | " ^
 	       "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
                "  Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
-    ("#Find"  ,["solutions v_i'''"])
+    ("#Find"  ,["solutions v'i'"])
    ],
    {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
     calc=[], crls=RootEq_crls, nrls=norm_Poly},
@@ -558,7 +558,7 @@
                 " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
 	        "(((rhs e_e) is_sqrtTerm_in (v_v::real))     & " ^
                 " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
-    ("#Find"  ,["solutions v_i'''"])
+    ("#Find"  ,["solutions v'i'"])
    ],
    {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
     prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly},
@@ -586,7 +586,7 @@
  (["RootEq","solve_right_sq_root_equation"],
    [("#Given" ,["equality e_e","solveFor v_v"]),
     ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
-    ("#Find"  ,["solutions v_i'''"])
+    ("#Find"  ,["solutions v'i'"])
    ],
    {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, 
     prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly},
@@ -611,7 +611,7 @@
  (["RootEq","solve_left_sq_root_equation"],
    [("#Given" ,["equality e_e","solveFor v_v"]),
     ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
-    ("#Find"  ,["solutions v_i'''"])
+    ("#Find"  ,["solutions v'i'"])
    ],
    {rew_ord'="termlessI",
     rls'=RootEq_erls,