# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1284459162 -7200
# Node ID b497233515336c9356cd7c1cf6e97c1ca045cf9a
# Parent  79b6cbd0268127bcfbdf01f35f25bc86708ad892
adapted is_copy_named from v___ to v'''

Unclear comment for 'fun is_copy_named_generating',
thus probably still broken; waiting for further tests.
Tests are still run from Build_Isac.

diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Build_Isac.thy
--- a/src/Tools/isac/Build_Isac.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Build_Isac.thy	Tue Sep 14 12:12:42 2010 +0200
@@ -85,8 +85,10 @@
   use_thy "Knowledge/Test"
 *)
 use_thy "Knowledge/Isac"
-check_guhs_unique := false;
+ML {* check_guhs_unique := false; *}
 ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
 
+use "../../../test/Tools/isac/Interpret/calchead.sml"
+
 end
 
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Interpret/calchead.sml
--- a/src/Tools/isac/Interpret/calchead.sml	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Interpret/calchead.sml	Tue Sep 14 12:12:42 2010 +0200
@@ -931,9 +931,10 @@
    of a SubProblem ? see ME/ptyps.sml 'type met '.*)
 fun is_copy_named_idstr str =
     case (rev o explode) str of
-	"_"::_::"_"::_ => true
+      (*"_"::_  ::"_"::_ => true*)
+	"'"::"'"::"'"::_ => true
       | _ => false;
-(*> is_copy_named_idstr "v_i_";
+(*> is_copy_named_idstr "v_i'''";
 val it = true : bool
   > is_copy_named_idstr "e_";
 val it = false : bool 
@@ -947,7 +948,7 @@
 	"_"::"_"::"_"::_ => false
       | _ => true
     else false;
-(*> is_copy_named_generating_idstr "v_i_";
+(*> is_copy_named_generating_idstr "v_i'''";
 val it = true : bool
   > is_copy_named_generating_idstr "L___";
 val it = false : bool
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Interpret/ptyps.sml
--- a/src/Tools/isac/Interpret/ptyps.sml	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Interpret/ptyps.sml	Tue Sep 14 12:12:42 2010 +0200
@@ -356,7 +356,7 @@
 (*.the pattern for an item of a problems model or a methods guard.*)
 type pat = (string *      (*field*)
 	     (term *       (*description*)
-	      term))       (*id | struct-var*);
+	      term))       (*id | arbitrary term*);
 fun pat2str ((field, (dsc, id)):pat) = 
     pair2str (field, pair2str (term2str dsc, term2str id));
 fun pats2str pats = (strs2str o (map pat2str)) pats;
@@ -376,7 +376,7 @@
       nrls       : rls,        (*canonical simplifier specific for this met  *)
       calc       : calc list,  (*040207: <--- calclist' in fun prep_met      *)
       (*branch   : TransitiveB set in append_problem at generation ob pblobj
-       FIXXXME.8.03: set branch from met in Apply_Method                     *)
+       FIXXXME.0308: set branch from met in Apply_Method ?                   *)
 
       (* compare type pbt:*)
       ppc: pat list,       
@@ -385,7 +385,7 @@
         are 'copy-named' with an identifier "*_!_".
         copy-named items are 'generating' if they are NOT "*___"
         see ME/calchead.sml 'fun is_copy_named'.*)
-      pre: term list,      (*preconditions in where*)
+      pre: term list,          (*preconditions in where*)
       (*script*)  
       scr: scr (*prep_met requires either script or string "empty_script"*)
 	   };
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Knowledge/Equation.thy
--- a/src/Tools/isac/Knowledge/Equation.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Knowledge/Equation.thy	Tue Sep 14 12:12:42 2010 +0200
@@ -44,7 +44,7 @@
  (["equation"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["matches (?a = ?b) e_e"]),
-   ("#Find"  ,["solutions v_i"])
+   ("#Find"  ,["solutions v_i'''"])
   ],
   append_rls "equation_prls" e_rls 
 	     [Calc ("Tools.matches",eval_matches "")],
@@ -56,7 +56,7 @@
  (["univariate","equation"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["matches (?a = ?b) e_e"]),
-   ("#Find"  ,["solutions v_i"])
+   ("#Find"  ,["solutions v_i'''"])
   ],
   univariate_equation_prls,SOME "solve (e_e::bool, v_v)",[]));
 
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Sep 14 12:12:42 2010 +0200
@@ -134,7 +134,7 @@
                "Not( (rhs e_e) is_polyrat_in v_v)",
                "((lhs e_e) has_degree_in v_v)=1",
 	       "((rhs e_e) has_degree_in v_v)=1"]),
-   ("#Find"  ,["solutions v_i"]) 
+   ("#Find"  ,["solutions v_i'''"]) 
   ],
   LinEq_prls, SOME "solve (e_e::bool, v_v)",
   [["LinEq","solve_lineq_equation"]]));
@@ -155,7 +155,7 @@
    [("#Given", ["equality e_e", "solveFor v_v"]),
     ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)",
                 "((lhs e_e)  has_degree_in v_v) = 1"]),
-    ("#Find",  ["solutions v_i"])
+    ("#Find",  ["solutions v_i'''"])
    ],
    {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls,
     calc=[], crls=LinEq_crls, nrls=norm_Poly},
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Knowledge/LogExp.thy
--- a/src/Tools/isac/Knowledge/LogExp.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Knowledge/LogExp.thy	Tue Sep 14 12:12:42 2010 +0200
@@ -33,9 +33,9 @@
  (["logarithmic","univariate","equation"],
   [("#Given",["equality e_e","solveFor v_v"]),
    ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
-   ("#Find" ,["solutions v_i"]),
-   ("#With" ,["||(lhs (Subst (v_i_,v_v) e_e) - " ^
-	      "  (rhs (Subst (v_i_,v_v) e_e) || < eps)"])
+   ("#Find" ,["solutions v_i'''"]),
+   ("#With" ,["||(lhs (Subst (v_i''', v_v) e_e) - " ^
+	      "  (rhs (Subst (v_i''', v_v) e_e) || < eps)"])
    ],
   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
   [["Equation","solve_log"]]));
@@ -47,7 +47,7 @@
  (["Equation","solve_log"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
-   ("#Find"  ,["solutions v_i"])
+   ("#Find"  ,["solutions v_i'''"])
   ],
    {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
     calc=[],crls=PolyEq_crls, nrls=norm_Rational},
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Knowledge/PolyEq.thy
--- a/src/Tools/isac/Knowledge/PolyEq.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Tue Sep 14 12:12:42 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_"))],
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Knowledge/RatEq.thy
--- a/src/Tools/isac/Knowledge/RatEq.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Knowledge/RatEq.thy	Tue Sep 14 12:12:42 2010 +0200
@@ -175,7 +175,7 @@
  (["rational","univariate","equation"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
-   ("#Find"  ,["solutions v_i"]) 
+   ("#Find"  ,["solutions v_i'''"]) 
   ],
 
   RatEq_prls, SOME "solve (e_e::bool, v_v)",
@@ -199,7 +199,7 @@
  (["RatEq","solve_rat_equation"],
    [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
-   ("#Find"  ,["solutions v_i"])
+   ("#Find"  ,["solutions v_i'''"])
   ],
    {rew_ord'="termlessI",
     rls'=rateq_erls,
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Knowledge/RootEq.thy
--- a/src/Tools/isac/Knowledge/RootEq.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Knowledge/RootEq.thy	Tue Sep 14 12:12:42 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,
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Knowledge/RootRatEq.thy
--- a/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Tue Sep 14 12:12:42 2010 +0200
@@ -144,7 +144,7 @@
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
 	       "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
-   ("#Find"  ,["solutions v_i"])
+   ("#Find"  ,["solutions v_i'''"])
    ],
   RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
   [["RootRatEq","elim_rootrat_equation"]]));
@@ -164,7 +164,7 @@
    [("#Given" ,["equality e_e","solveFor v_v"]),
     ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
 	       "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
-    ("#Find"  ,["solutions v_i"])
+    ("#Find"  ,["solutions v_i'''"])
    ],
    {rew_ord'="termlessI",
     rls'=RooRatEq_erls,
diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Tue Sep 14 12:12:42 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_i'''"])
   ],
   assoc_rls "matches",
   SOME "solve (e_e::bool, v_v)", []));
@@ -532,7 +532,7 @@
  (["univariate","equation","test"],
   [("#Given" ,["equality e_e","solveFor v_v"]),
    ("#Where" ,["matches (?a = ?b) e_e"]),
-   ("#Find"  ,["solutions v_i"])
+   ("#Find"  ,["solutions 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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_i'''"]) 
    ],
    {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
    calc=[],
diff -r 79b6cbd02681 -r b49723351533 test/Tools/isac/Interpret/calchead.sml
--- a/test/Tools/isac/Interpret/calchead.sml	Mon Sep 13 18:37:16 2010 +0200
+++ b/test/Tools/isac/Interpret/calchead.sml	Tue Sep 14 12:12:42 2010 +0200
@@ -10,6 +10,7 @@
 "-----------------------------------------------------------------";
 "table of contents -----------------------------------------------";
 "-----------------------------------------------------------------";
+"--------- regression test fun is_copy_named ---------------------";
 "--------- get_interval after replace} other 2 -------------------";
 "--------- maximum example with 'specify' ------------------------";
 "--------- maximum example with 'specify', fmz <> [] -------------";
@@ -20,6 +21,24 @@
 "-----------------------------------------------------------------";
 
 
+"--------- regression test fun is_copy_named ---------------------";
+"--------- regression test fun is_copy_named ---------------------";
+"--------- regression test fun is_copy_named ---------------------";
+val trm = (1, (2, @{term "v_i'''"}));
+if is_copy_named trm then () else raise error "regr. is_copy_named";
+val trm = (1, (2, @{term "e_e"}));
+if is_copy_named trm then raise error "regr. is_copy_named" else ();
+val trm = (1, (2, @{term "L'''"}));
+if is_copy_named trm then () else raise error "regr. is_copy_named";
+
+(* out-comment 'structure CalcHead'...
+val trm = (1, (2, @{term "v_i'''"}));
+if is_copy_named_generating trm then () else raise error "regr. is_copy_named";
+val trm = (1, (2, @{term "L'''"}));
+if is_copy_named_generating trm then raise error "regr. is_copy_named" else ();
+*)
+
+(*==========================================================================
 "--------- get_interval after replace} other 2 -------------------";
 "--------- get_interval after replace} other 2 -------------------";
 "--------- get_interval after replace} other 2 -------------------";
@@ -411,3 +430,5 @@
     (*         type of Find:             [Free ("x_i", "bool List.list")]*)
     => ()
   | _ => raise error "calchead.sml match_ags [univariate,equation,test]--";
+
+==========================================================================*)
diff -r 79b6cbd02681 -r b49723351533 test/Tools/isac/ProgLang/term.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/test/Tools/isac/ProgLang/term.sml	Tue Sep 14 12:12:42 2010 +0200
@@ -0,0 +1,168 @@
+(* tests on Scripts/term_G.sml
+   author: Walther Neuper
+   051006,
+   (c) due to copyright terms
+
+use"../smltest/Scripts/term_G.sml";
+use"term_G.sml";
+*)
+
+"-----------------------------------------------------------------";
+"table of contents -----------------------------------------------";
+"-----------------------------------------------------------------";
+"----------- inst_bdv --------------------------------------------";
+"----------- subst_atomic_all ------------------------------------";
+"----------- Pattern.match ---------------------------------------";
+"----------- fun matches -----------------------------------------";
+"------------parse------------------------------------------------";
+"----------- uminus_to_string ------------------------------------";
+"-----------------------------------------------------------------";
+"-----------------------------------------------------------------";
+
+
+"----------- inst_bdv --------------------------------------------";
+"----------- inst_bdv --------------------------------------------";
+"----------- inst_bdv --------------------------------------------";
+if string_of_thm (num_str @{thm d1_isolate_add2}) = 
+    "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
+else raise error "term_G.sml d1_isolate_add2";
+val subst = [(str2term "bdv", str2term "x")];
+val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
+val t' = inst_bdv subst t;
+if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
+else raise error "term_G.sml inst_bdv 1";
+
+if string_of_thm (num_str @{thm separate_bdvs_add}) = 
+   "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
+   \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
+else raise error "term_G.sml separate_bdvs_add";
+val subst = [(str2term"bdv_1",str2term"c"),
+	    (str2term"bdv_2",str2term"c_2"),
+	    (str2term"bdv_3",str2term"c_3"),
+	    (str2term"bdv_4",str2term"c_4")];
+val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
+val t' = inst_bdv subst t;
+if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
+		 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
+else raise error "term_G.sml inst_bdv 2";
+
+
+"----------- subst_atomic_all ------------------------------------";
+"----------- subst_atomic_all ------------------------------------";
+"----------- subst_atomic_all ------------------------------------";
+val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
+val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
+	   (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
+val (all_Free_subst, t') = subst_atomic_all env t;
+if all_Free_subst andalso 
+   term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
+else raise error "term_G.sml subst_atomic_all should be 'true'";
+
+
+val (all_Free_subst, t') = subst_atomic_all (tl env) t;
+if not all_Free_subst andalso 
+   term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
+else raise error "term_G.sml subst_atomic_all should be 'false'";
+
+
+"----------- Pattern.match ---------------------------------------";
+"----------- Pattern.match ---------------------------------------";
+"----------- Pattern.match ---------------------------------------";
+val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
+val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
+(*        !^^^^^^^^!... necessary for Pattern.match*)
+val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
+(*val insts =
+  ([],
+   [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
+    (("a",0),Free ("3","RealDef.real"))])
+  : (indexname * typ) list * (indexname * term) list*)
+
+"----- throws exn MATCH...";
+val t = str2term "x";
+(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)) 
+handle MATCH => ([(* (Term.indexname * Term.typ) *)],
+		 [(* (Term.indexname * Term.term) *)]);
+Pattern.MATCH;
+
+(*ML {**)
+val thy = @{theory "Complex_Main"};
+val PARSE = Syntax.read_term_global thy;
+val (pa, tm) = (PARSE "a + b::real", PARSE  "x + 2*z::real");
+"-------";
+val (tye, tme) = 
+  (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
+"-------";
+val (tye, tme) = Pattern.match thy (Logic.varify pa, tm) (Vartab.empty, 
+							  Vartab.empty);
+"-------";
+val (tyenv, tenv) = Pattern.match thy (Logic.varify pa, tm)
+				  (Vartab.empty, Vartab.empty);
+Vartab.dest tenv;
+match thy tm (Logic.varify pa);
+
+(**}*)
+
+"----------- fun matches -----------------------------------------";
+"----------- fun matches -----------------------------------------";
+"----------- fun matches -----------------------------------------";
+(*smltest/IsacKnowledge/polyeq.sml:     
+  Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
+(*smltest/ME/ptyps.sml:        
+  |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
+(*ML {**) 
+val thy = @{theory "Complex_Main"};
+"----- test 1";
+val pa = Logic.varify @{term "a = (0::real)"};
+"----- test 1 true";
+val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"};
+if matches thy tm pa then () 
+  else error "term_G.sml diff.behav. in matches true";
+"----- test 2 false";
+val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};
+if matches thy tm pa then error "term_G.sml diff.behav. in matches false"
+  else ();
+(**}*)
+
+"------------parse------------------------------------------------";
+"------------parse------------------------------------------------";
+"------------parse------------------------------------------------";
+(*ML {**)
+Toplevel.debug := true;
+(* literal types:
+PolyML.addPrettyPrinter
+  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
+*)(* pretty types:
+PolyML.addPrettyPrinter
+  (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
+print_depth 99;
+*)
+val thy = @{theory "Complex_Main"};
+val str = "x + z";
+parse thy str;
+"---------------";
+val str = "x + 2*z";
+val t = (Syntax.read_term_global thy str);
+val t = numbers_to_string (Syntax.read_term_global thy str);
+val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
+cterm_of thy t;
+val t = (the (parse thy str)) handle _ => error "term_G.sml parsing 'x + 2*z' failed";
+(**}*)
+(*Makarius.1003
+ML {* @{term "2::int"} *}
+
+term "(1.24444) :: real"
+
+ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
+*)
+
+
+"----------- uminus_to_string ------------------------------------";
+"----------- uminus_to_string ------------------------------------";
+"----------- uminus_to_string ------------------------------------";
+(*ML {*)
+val t1 = numbers_to_string @{term "-2::real"};
+val t2 = numbers_to_string @{term "- 2::real"};
+if uminus_to_string t2 = t1 then ()
+else error "term_G.sml diff.behav. in uminus_to_string";
+(*}*)
diff -r 79b6cbd02681 -r b49723351533 test/Tools/isac/ProgLang/term_G.sml
--- a/test/Tools/isac/ProgLang/term_G.sml	Mon Sep 13 18:37:16 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,168 +0,0 @@
-(* tests on Scripts/term_G.sml
-   author: Walther Neuper
-   051006,
-   (c) due to copyright terms
-
-use"../smltest/Scripts/term_G.sml";
-use"term_G.sml";
-*)
-
-"-----------------------------------------------------------------";
-"table of contents -----------------------------------------------";
-"-----------------------------------------------------------------";
-"----------- inst_bdv --------------------------------------------";
-"----------- subst_atomic_all ------------------------------------";
-"----------- Pattern.match ---------------------------------------";
-"----------- fun matches -----------------------------------------";
-"------------parse------------------------------------------------";
-"----------- uminus_to_string ------------------------------------";
-"-----------------------------------------------------------------";
-"-----------------------------------------------------------------";
-
-
-"----------- inst_bdv --------------------------------------------";
-"----------- inst_bdv --------------------------------------------";
-"----------- inst_bdv --------------------------------------------";
-if string_of_thm (num_str @{thm d1_isolate_add2}) = 
-    "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
-else raise error "term_G.sml d1_isolate_add2";
-val subst = [(str2term "bdv", str2term "x")];
-val t = (norm o #prop o rep_thm) (num_str @{thm d1_isolate_add2});
-val t' = inst_bdv subst t;
-if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
-else raise error "term_G.sml inst_bdv 1";
-
-if string_of_thm (num_str @{thm separate_bdvs_add}) = 
-   "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
-   \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
-else raise error "term_G.sml separate_bdvs_add";
-val subst = [(str2term"bdv_1",str2term"c"),
-	    (str2term"bdv_2",str2term"c_2"),
-	    (str2term"bdv_3",str2term"c_3"),
-	    (str2term"bdv_4",str2term"c_4")];
-val t = (norm o #prop o rep_thm) (num_str @{thm separate_bdvs_add});
-val t' = inst_bdv subst t;
-if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
-		 \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
-else raise error "term_G.sml inst_bdv 2";
-
-
-"----------- subst_atomic_all ------------------------------------";
-"----------- subst_atomic_all ------------------------------------";
-"----------- subst_atomic_all ------------------------------------";
-val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
-val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
-	   (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
-val (all_Free_subst, t') = subst_atomic_all env t;
-if all_Free_subst andalso 
-   term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
-else raise error "term_G.sml subst_atomic_all should be 'true'";
-
-
-val (all_Free_subst, t') = subst_atomic_all (tl env) t;
-if not all_Free_subst andalso 
-   term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
-else raise error "term_G.sml subst_atomic_all should be 'false'";
-
-
-"----------- Pattern.match ---------------------------------------";
-"----------- Pattern.match ---------------------------------------";
-"----------- Pattern.match ---------------------------------------";
-val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
-val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
-(*        !^^^^^^^^!... necessary for Pattern.match*)
-val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
-(*val insts =
-  ([],
-   [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
-    (("a",0),Free ("3","RealDef.real"))])
-  : (indexname * typ) list * (indexname * term) list*)
-
-"----- throws exn MATCH...";
-val t = str2term "x";
-(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)) 
-handle MATCH => ([(* (Term.indexname * Term.typ) *)],
-		 [(* (Term.indexname * Term.term) *)]);
-Pattern.MATCH;
-
-(*ML {**)
-val thy = @{theory "Complex_Main"};
-val PARSE = Syntax.read_term_global thy;
-val (pa, tm) = (PARSE "a + b::real", PARSE  "x + 2*z::real");
-"-------";
-val (tye, tme) = 
-  (Vartab.empty : Type.tyenv, Vartab.empty : Envir.tenv);
-"-------";
-val (tye, tme) = Pattern.match thy (Logic.varify pa, tm) (Vartab.empty, 
-							  Vartab.empty);
-"-------";
-val (tyenv, tenv) = Pattern.match thy (Logic.varify pa, tm)
-				  (Vartab.empty, Vartab.empty);
-Vartab.dest tenv;
-match thy tm (Logic.varify pa);
-
-(**}*)
-
-"----------- fun matches -----------------------------------------";
-"----------- fun matches -----------------------------------------";
-"----------- fun matches -----------------------------------------";
-(*smltest/IsacKnowledge/polyeq.sml:     
-  Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)"*)
-(*smltest/ME/ptyps.sml:        
-  |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],*)
-(*ML {**) 
-val thy = @{theory "Complex_Main"};
-"----- test 1";
-val pa = Logic.varify @{term "a = (0::real)"};
-"----- test 1 true";
-val tm = @{term "-8 - 2 * x + x ^ 2 = (0::real)"};
-if matches thy tm pa then () 
-  else error "term_G.sml diff.behav. in matches true";
-"----- test 2 false";
-val tm = @{term "-8 - 2 * x + x ^ 2 = (3::real)"};
-if matches thy tm pa then error "term_G.sml diff.behav. in matches false"
-  else ();
-(**}*)
-
-"------------parse------------------------------------------------";
-"------------parse------------------------------------------------";
-"------------parse------------------------------------------------";
-(*ML {**)
-Toplevel.debug := true;
-(* literal types:
-PolyML.addPrettyPrinter
-  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ);
-*)(* pretty types:
-PolyML.addPrettyPrinter
-  (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
-print_depth 99;
-*)
-val thy = @{theory "Complex_Main"};
-val str = "x + z";
-parse thy str;
-"---------------";
-val str = "x + 2*z";
-val t = (Syntax.read_term_global thy str);
-val t = numbers_to_string (Syntax.read_term_global thy str);
-val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
-cterm_of thy t;
-val t = (the (parse thy str)) handle _ => error "term_G.sml parsing 'x + 2*z' failed";
-(**}*)
-(*Makarius.1003
-ML {* @{term "2::int"} *}
-
-term "(1.24444) :: real"
-
-ML {* numbers_to_string @{term "%x. (-9993::int) + x + 1"} *}
-*)
-
-
-"----------- uminus_to_string ------------------------------------";
-"----------- uminus_to_string ------------------------------------";
-"----------- uminus_to_string ------------------------------------";
-(*ML {*)
-val t1 = numbers_to_string @{term "-2::real"};
-val t2 = numbers_to_string @{term "- 2::real"};
-if uminus_to_string t2 = t1 then ()
-else error "term_G.sml diff.behav. in uminus_to_string";
-(*}*)
diff -r 79b6cbd02681 -r b49723351533 test/Tools/isac/Run_Tests.thy
--- a/test/Tools/isac/Run_Tests.thy	Mon Sep 13 18:37:16 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*
-$ cd /usr/local/isabisac/test/Tools/isac
-$ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy &
-
-*)
-
-theory Run_Tests imports Main begin
-
-use "ProgLang/term.sml"
-
-end
diff -r 79b6cbd02681 -r b49723351533 test/Tools/isac/Test_Isac.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/test/Tools/isac/Test_Isac.thy	Tue Sep 14 12:12:42 2010 +0200
@@ -0,0 +1,111 @@
+(* Title Run_Tests on isac
+$ cd /usr/local/isabisac/test/Tools/isac
+$ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy &
+
+was sml/RTEST-root.sml in isac-2002
+*)
+
+theory Test_Isac imports Isac begin
+ 
+ML{* writeln "**** run the tests **************************************" *};
+(* 
+cd "systest";
+(*+ check kbtest/diffapp.sml for additional items in met-model*)
+       	use"root-equ.sml"; 
+       	use"script.sml";   
+	(* use"script_if.sml"; WN03 missing: is_rootequation_in*)
+       	use"scriptnew.sml";     
+       	use"subp-rooteq.sml";   
+	use"tacis.sml";
+	use"interface-xml.sml";
+	(* use"testdaten.sml"; no update after dropping 'errorBound'*)    
+ 	cd "../..";
+*)
+ML{* writeln "**** run systests complete ******************************" *};
+(*
+cd"smltest/Scripts";
+ 	use"calculate-float.sml";
+ 	use"calculate.sml";
+	use"listg.sml";
+	use"rewrite.sml";
+ 	use"scrtools.sml";
+        use"term.sml";
+ 	use"tools.sml";
+ 	cd "../.."; 
+cd"smltest/ME";
+        use"ctree.sml";
+*)
+use "Interpret/calchead.sml"
+(*
+       	use"calchead.sml"; 
+ 	use"rewtools.sml";
+        use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
+        use"inform.sml";
+	use"me.sml";
+       	use"ptyps.sml"; 
+ 	cd "../.."; 
+cd"smltest/xmlsrc";
+ 	use"datatypes.sml";        
+       	use"pbl-met-hierarchy.sml"; 
+       	use"thy-hierarchy.sml"; 
+ 	cd "../.."; 
+cd"smltest/FE-interface";
+       	use"interface.sml";
+ 	cd "../..";
+*)
+ML{* writeln "**** run tests on math-engine complete ******************" *};
+(*
+cd"smltest/IsacKnowledge";
+        use"atools.sml";
+ 	use"complex.sml";
+ 	use"diff.sml";
+ 	use"diffapp.sml";
+	use"integrate.sml";
+	use"equation.sml";
+	(*use"inssort.sml"; problems with recdef in Isabelle2002*)
+ 	use"logexp.sml";
+ 	use"poly.sml";
+ 	use"polyminus.sml";
+ 	use"polyeq.sml";  (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
+ 			     ? also check others without check 'diff.behav.'*);
+ 	use"rateq.sml";
+ 	use"rational.sml" (*TODO add_fractions_p throws overflow-exn      WN*);
+ 	use"rlang.sml";    (*WN.12.6.03: for TODOs search 'writeln', 
+ 			     for simplification search MG 
+ 		 erls:       98a(1) 104a(1) 104a(2) 68a *);
+ 	use"root.sml";
+ 	use"rooteq.sml";
+ 	use"rootrateq.sml";
+ 	use"termorder.sml";
+ 	use"trig.sml";
+ 	use"vect.sml";  
+	use"wn.sml";
+	use"eqsystem.sml";
+	use"biegelinie.sml";
+	use"algein.sml";
+ 	cd "../..";
+*)
+ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
+(*
+val path = "/home/neuper/proto2/testsml2xml/"; 
+pbl_hierarchy2file (path ^ "pbl/");
+pbls2file          (path ^ "pbl/");
+met_hierarchy2file (path ^ "met/");
+mets2file          (path ^ "met/");
+thy_hierarchy2file (path ^ "thy/");
+thes2file          (path ^ "thy/");
+cd"sml";
+*)
+ML{* writeln "**** tested creation of xmldata *************************" *};
+
+ML{*states:=[];
+     writeln "=========================================================";
+     
+     writeln "**** run systests complete ***************** re-organize!";
+     writeln "**** run tests on math-engine complete ******************";
+     writeln "**** run tests on IsacKnowledge complete ****************";
+     writeln "**** build isac kernel + run tests complete *************";
+     writeln "**** tested creation of xmldata *************************";
+*}
+
+end