diff -r b49723351533 -r a37a3ab989f4 src/Tools/isac/Knowledge/PolyEq.thy
--- a/src/Tools/isac/Knowledge/PolyEq.thy	Tue Sep 14 12:12:42 2010 +0200
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Tue Sep 14 15:46:56 2010 +0200
@@ -849,7 +849,7 @@
    ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
 	       "~((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'"])
    ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   []));
@@ -862,7 +862,7 @@
 	       "(lhs e_e) is_poly_in v_v",
 	       "((lhs e_e) has_degree_in v_v ) = 0"
 	      ]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","solve_d0_polyeq_equation"]]));
@@ -876,7 +876,7 @@
 	       "(lhs e_e) is_poly_in v_v",
 	       "((lhs e_e) has_degree_in v_v ) = 1"
 	      ]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","solve_d1_polyeq_equation"]]));
@@ -890,7 +890,7 @@
    ("#Where" ,["matches (?a = 0) e_e",
 	       "(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v ) = 2"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","solve_d2_polyeq_equation"]]));
@@ -911,7 +911,7 @@
 	       "Not (matches (     ?b*?v_ +    ?v_^^^2 = 0) e_e) &" ^
 	       "Not (matches (        ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
 	       "Not (matches (     ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
@@ -926,7 +926,7 @@
 	       "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^
 	       "matches (            ?v_^^^2 = 0) e_e | " ^
 	       "matches (         ?b*?v_^^^2 = 0) e_e "]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
@@ -937,7 +937,7 @@
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
 	       "matches (?a +   ?v_^^^2 = 0) e_e"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","solve_d2_polyeq_pq_equation"]]));
@@ -948,7 +948,7 @@
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["matches (?a +    ?v_^^^2 = 0) e_e | " ^
 	       "matches (?a + ?b*?v_^^^2 = 0) e_e"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","solve_d2_polyeq_abc_equation"]]));
@@ -962,7 +962,7 @@
    ("#Where" ,["matches (?a = 0) e_e",
 	       "(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 3"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","solve_d3_polyeq_equation"]]));
@@ -975,7 +975,7 @@
    ("#Where" ,["matches (?a = 0) e_e",
 	       "(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 4"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [(*["PolyEq","solve_d4_polyeq_equation"]*)]));
@@ -987,7 +987,7 @@
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
 	       "(Not(((lhs e_e) is_poly_in v_v)))"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","normalize_poly"]]));
@@ -998,7 +998,7 @@
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["matches (?a = 0) e_e",
 	       "(lhs e_e) is_expanded_in v_v "]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
    ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   []));
@@ -1009,7 +1009,7 @@
  (["degree_2","expanded","univariate","equation"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["PolyEq","complete_square"]]));
@@ -1043,7 +1043,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |" ^
 	       "(Not(((lhs e_e) is_poly_in v_v)))"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI",
     rls'=PolyEq_erls,
@@ -1070,7 +1070,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 0"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI",
     rls'=PolyEq_erls,
@@ -1091,7 +1091,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 1"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
@@ -1112,7 +1112,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 2"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI",
     rls'=PolyEq_erls,
@@ -1139,7 +1139,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 2"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI",
     rls'=PolyEq_erls,
@@ -1166,7 +1166,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 2"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI",
     rls'=PolyEq_erls,
@@ -1190,7 +1190,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 2"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI",
     rls'=PolyEq_erls,
@@ -1214,7 +1214,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 2"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI",
     rls'=PolyEq_erls,
@@ -1238,7 +1238,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(lhs e_e) is_poly_in v_v ",
 	       "((lhs e_e) has_degree_in v_v) = 3"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI",
     rls'=PolyEq_erls,
@@ -1271,7 +1271,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["matches (?a = 0) e_e", 
 	       "((lhs e_e) has_degree_in v_v) = 2"]),
-   ("#Find"  ,["solutions v_i'''"])
+   ("#Find"  ,["solutions v'i'"])
   ],
    {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],