diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Thu Sep 23 08:43:36 2010 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Thu Sep 23 08:54:26 2010 +0200
@@ -522,7 +522,7 @@
  (["equation","test"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["matches (?a = ?b) e_e"]),
-   ("#Find"  ,["solutions v'i'"])
+   ("#Find"  ,["solutions v_v'i'"])
   ],
   assoc_rls "matches",
   SOME "solve (e_e::bool, v_v)", []));
@@ -543,7 +543,7 @@
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(matches (   v_v = 0) e_e) | (matches (   ?b*v_v = 0) e_e) |" ^
 	       "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e)  "]),
-   ("#Find"  ,["solutions v'i'"])
+   ("#Find"  ,["solutions v_v'i'"])
   ],
   assoc_rls "matches", 
   SOME "solve (e_e::bool, v_v)", [["Test","solve_linear"]]));
@@ -595,7 +595,7 @@
  (["Test","solve_linear"]:metID,
   [("#Given" ,["equality e_e","solveFor v_v"]),
     ("#Where" ,["matches (?a = ?b) e_e"]),
-    ("#Find"  ,["solutions v'i'"])
+    ("#Find"  ,["solutions v_v'i'"])
     ],
    {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
     prls = assoc_rls "matches", calc = [], crls = tval_rls,
@@ -783,7 +783,7 @@
 	       "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^
 	       "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^
 	       "(matches (        v_v ^^^2 = 0) e_e)"]),
-   ("#Find"  ,["solutions v'i'"])
+   ("#Find"  ,["solutions v_v'i'"])
   ],
   assoc_rls "matches", 
   SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
@@ -817,7 +817,7 @@
  (["polynomial","univariate","equation","test"],
   [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
    ("#Where" ,["False"]),
-   ("#Find"  ,["solutions v'i'"]) 
+   ("#Find"  ,["solutions v_v'i'"]) 
   ],
   e_rls, SOME "solve (e_e::bool, v_v)", []));
 
@@ -825,7 +825,7 @@
  (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
  (["degree_two","polynomial","univariate","equation","test"],
   [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
-   ("#Find"  ,["solutions v'i'"]) 
+   ("#Find"  ,["solutions v_v'i'"]) 
   ],
   e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
 
@@ -833,7 +833,7 @@
  (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
  (["pq_formula","degree_two","polynomial","univariate","equation","test"],
   [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
-   ("#Find"  ,["solutions v'i'"]) 
+   ("#Find"  ,["solutions v_v'i'"]) 
   ],
   e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
 
@@ -841,7 +841,7 @@
  (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
  (["abc_formula","degree_two","polynomial","univariate","equation","test"],
   [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
-   ("#Find"  ,["solutions v'i'"]) 
+   ("#Find"  ,["solutions v_v'i'"]) 
   ],
   e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
 
@@ -852,7 +852,7 @@
  (["squareroot","univariate","equation","test"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["contains_root (e_e::bool)"]),
-   ("#Find"  ,["solutions v'i'"]) 
+   ("#Find"  ,["solutions v_v'i'"]) 
   ],
   append_rls "contains_root" e_rls [Calc ("Test.contains'_root",
 			  eval_contains_root "#contains_root_")], 
@@ -863,7 +863,7 @@
  (["normalize","univariate","equation","test"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,[]),
-   ("#Find"  ,["solutions v'i'"]) 
+   ("#Find"  ,["solutions v_v'i'"]) 
   ],
   e_rls, SOME "solve (e_e::bool, v_v)", [["Test","norm_univar_equation"]]));
 
@@ -872,7 +872,7 @@
  (["sqroot-test","univariate","equation","test"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    (*("#Where" ,["contains_root (e_e::bool)"]),*)
-   ("#Find"  ,["solutions v'i'"]) 
+   ("#Find"  ,["solutions v_v'i'"]) 
   ],
   e_rls, SOME "solve (e_e::bool, v_v)", []));
 
@@ -889,7 +889,7 @@
  (["Test","sqrt-equ-test"]:metID,
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["contains_root (e_e::bool)"]),
-   ("#Find"  ,["solutions v'i'"])
+   ("#Find"  ,["solutions v_v'i'"])
    ],
   {rew_ord'="e_rew_ord",rls'=tval_rls,
    srls =append_rls "srls_contains_root" e_rls 
@@ -923,7 +923,7 @@
 (*root-equation ... for test-*.sml until 8.01*)
  (["Test","squ-equ-test2"]:metID,
   [("#Given" ,["equality e_e","solveFor v_v"]),
-   ("#Find"  ,["solutions v'i'"])
+   ("#Find"  ,["solutions v_v'i'"])
    ],
   {rew_ord'="e_rew_ord",rls'=tval_rls,
    srls = append_rls "srls_contains_root" e_rls 
@@ -957,7 +957,7 @@
 (*tests subproblem fixed linear*)
  (["Test","squ-equ-test-subpbl1"]:metID,
   [("#Given" ,["equality e_e","solveFor v_v"]),
-   ("#Find"  ,["solutions v'i'"])
+   ("#Find"  ,["solutions v_v'i'"])
    ],
   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
     crls=tval_rls, nrls=Test_simplify},
@@ -978,7 +978,7 @@
  (*tests subproblem fixed degree 2*)
  (["Test","squ-equ-test-subpbl2"]:metID,
   [("#Given" ,["equality e_e","solveFor v_v"]),
-   ("#Find"  ,["solutions v'i'"])
+   ("#Find"  ,["solutions v_v'i'"])
    ],
   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
     crls=tval_rls, nrls=e_rls(*,
@@ -998,7 +998,7 @@
  (*root-equation: see foils..., but notTerminating*)
  (["Test","square_equation...notTerminating"]:metID,
   [("#Given" ,["equality e_e","solveFor v_v"]),
-   ("#Find"  ,["solutions v'i'"])
+   ("#Find"  ,["solutions v_v'i'"])
    ],
   {rew_ord'="e_rew_ord",rls'=tval_rls,
    srls = append_rls "srls_contains_root" e_rls 
@@ -1031,7 +1031,7 @@
 (*root-equation1:*)
  (["Test","square_equation1"]:metID,
    [("#Given" ,["equality e_e","solveFor v_v"]),
-    ("#Find"  ,["solutions v'i'"])
+    ("#Find"  ,["solutions v_v'i'"])
     ],
    {rew_ord'="e_rew_ord",rls'=tval_rls,
    srls = append_rls "srls_contains_root" e_rls 
@@ -1063,7 +1063,7 @@
  (*root-equation2*)
  (["Test","square_equation2"]:metID,
    [("#Given" ,["equality e_e","solveFor v_v"]),
-    ("#Find"  ,["solutions v'i'"])
+    ("#Find"  ,["solutions v_v'i'"])
     ],
    {rew_ord'="e_rew_ord",rls'=tval_rls,
    srls = append_rls "srls_contains_root" e_rls 
@@ -1096,7 +1096,7 @@
  (*root-equation*)
  (["Test","square_equation"]:metID,
    [("#Given" ,["equality e_e","solveFor v_v"]),
-    ("#Find"  ,["solutions v'i'"])
+    ("#Find"  ,["solutions v_v'i'"])
     ],
    {rew_ord'="e_rew_ord",rls'=tval_rls,
    srls = append_rls "srls_contains_root" e_rls 
@@ -1133,7 +1133,7 @@
 	       "(matches (     ?b*v_v ^^^2 = 0) e_e) |" ^
 	       "(matches (?a +    v_v ^^^2 = 0) e_e) |" ^
 	       "(matches (        v_v ^^^2 = 0) e_e)"]), 
-   ("#Find"  ,["solutions v'i'"]) 
+   ("#Find"  ,["solutions v_v'i'"]) 
    ],
    {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
     prls = assoc_rls "matches",
@@ -1155,7 +1155,7 @@
  (["Test","norm_univar_equation"]:metID,
    [("#Given",["equality e_e","solveFor v_v"]),
    ("#Where" ,[]), 
-   ("#Find"  ,["solutions v'i'"]) 
+   ("#Find"  ,["solutions v_v'i'"]) 
    ],
    {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
    calc=[],