# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1283941558 -7200
# Node ID bf83d30839c7ab2e45cd4e470cac7f77ec089114
# Parent  7b1d2366c191dd763fb0bbb6a8ea4edea680ff02
tuned

diff -r 7b1d2366c191 -r bf83d30839c7 src/Tools/isac/Knowledge/RootEq.thy
--- a/src/Tools/isac/Knowledge/RootEq.thy	Wed Sep 08 12:10:43 2010 +0200
+++ b/src/Tools/isac/Knowledge/RootEq.thy	Wed Sep 08 12:25:58 2010 +0200
@@ -542,7 +542,7 @@
     "           (Try (Rewrite_Set rooteq_simplify              True)) @@  " ^ 
     "           (Try (Repeat (Rewrite_Set make_rooteq        False))) @@  " ^
     "           (Try (Rewrite_Set rooteq_simplify              True))) e_e " ^
-    " in ((SubProblem (RootEq_',[univariate,equation],                     " ^
+    " in ((SubProblem (RootEq',[univariate,equation],                     " ^
     "      [no_met]) [BOOL e_e, REAL v_v])))"
    ));
 
@@ -571,9 +571,9 @@
 "   (Try (Rewrite_Set rooteq_simplify                    True)) ) e_e;   " ^
 " (L_L::bool list) =                                                     " ^
 "   (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
-"    then (SubProblem (RootEq_',[normalize,root',univariate,equation],   " ^
+"    then (SubProblem (RootEq',[normalize,root',univariate,equation],   " ^
 "                      [no_met]) [BOOL e_e, REAL v_v])                   " ^
-"    else (SubProblem (RootEq_',[univariate,equation], [no_met])         " ^
+"    else (SubProblem (RootEq',[univariate,equation], [no_met])         " ^
 "                     [BOOL e_e, REAL v_v]))                             " ^
 "in Check_elementwise L_L {(v_v::real). Assumptions})"
  ));
@@ -598,9 +598,9 @@
    "    (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@   " ^
    "    (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
    " in if ((rhs e_e) is_sqrtTerm_in v_v)                                    " ^
-   " then (SubProblem (RootEq_',[normalize,root',univariate,equation],       " ^
+   " then (SubProblem (RootEq',[normalize,root',univariate,equation],       " ^
    "       [no_met]) [BOOL e_e, REAL v_v])                                   " ^
-   " else ((SubProblem (RootEq_',[univariate,equation],                      " ^
+   " else ((SubProblem (RootEq',[univariate,equation],                      " ^
    "        [no_met]) [BOOL e_e, REAL v_v])))"
  ));
 val --------------------------------------------------+++ = "33333";
@@ -627,9 +627,9 @@
     "  (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@  " ^
     "  (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
     " in if ((lhs e_e) is_sqrtTerm_in v_v)                                   " ^ 
-    " then (SubProblem (RootEq_',[normalize,root',univariate,equation],      " ^
+    " then (SubProblem (RootEq',[normalize,root',univariate,equation],      " ^
     "       [no_met]) [BOOL e_e, REAL v_v])                                " ^
-    " else ((SubProblem (RootEq_',[univariate,equation],                    " ^
+    " else ((SubProblem (RootEq',[univariate,equation],                    " ^
     "        [no_met]) [BOOL e_e, REAL v_v])))"
    ));
 val --------------------------------------------------++++ = "44444";
diff -r 7b1d2366c191 -r bf83d30839c7 src/Tools/isac/Knowledge/RootRatEq.thy
--- a/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Sep 08 12:10:43 2010 +0200
+++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Sep 08 12:25:58 2010 +0200
@@ -175,7 +175,7 @@
     "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^
     "           (Try (Rewrite_Set_Inst [(bdv,v_)]               " ^
     "                                  rootrat_solve False))) e_e " ^
-    " in (SubProblem (RootEq_,[univariate,equation],            " ^
+    " in (SubProblem (RootEq',[univariate,equation],            " ^
     "        [no_met]) [BOOL e_e, REAL v_]))"
    ));
 calclist':= overwritel (!calclist',