Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
tuned isac-update-Isa09-2
authorWalther Neuper <neuper@ist.tugraz.at>
Wed, 08 Sep 2010 12:25:58 +0200
branchisac-update-Isa09-2
changeset 37987bf83d30839c7
parent 37986 7b1d2366c191
child 37988 03e6d5db883e
tuned
src/Tools/isac/Knowledge/RootEq.thy file | annotate | diff | comparison | revisions
src/Tools/isac/Knowledge/RootRatEq.thy file | annotate | diff | comparison | revisions 
     1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Wed Sep 08 12:10:43 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Wed Sep 08 12:25:58 2010 +0200
     1.3 @@ -542,7 +542,7 @@
     1.4      "           (Try (Rewrite_Set rooteq_simplify              True)) @@  " ^ 
     1.5      "           (Try (Repeat (Rewrite_Set make_rooteq        False))) @@  " ^
     1.6      "           (Try (Rewrite_Set rooteq_simplify              True))) e_e " ^
     1.7 -    " in ((SubProblem (RootEq_',[univariate,equation],                     " ^
     1.8 +    " in ((SubProblem (RootEq',[univariate,equation],                     " ^
     1.9      "      [no_met]) [BOOL e_e, REAL v_v])))"
    1.10     ));
    1.11  
    1.12 @@ -571,9 +571,9 @@
    1.13  "   (Try (Rewrite_Set rooteq_simplify                    True)) ) e_e;   " ^
    1.14  " (L_L::bool list) =                                                     " ^
    1.15  "   (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
    1.16 -"    then (SubProblem (RootEq_',[normalize,root',univariate,equation],   " ^
    1.17 +"    then (SubProblem (RootEq',[normalize,root',univariate,equation],   " ^
    1.18  "                      [no_met]) [BOOL e_e, REAL v_v])                   " ^
    1.19 -"    else (SubProblem (RootEq_',[univariate,equation], [no_met])         " ^
    1.20 +"    else (SubProblem (RootEq',[univariate,equation], [no_met])         " ^
    1.21  "                     [BOOL e_e, REAL v_v]))                             " ^
    1.22  "in Check_elementwise L_L {(v_v::real). Assumptions})"
    1.23   ));
    1.24 @@ -598,9 +598,9 @@
    1.25     "    (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@   " ^
    1.26     "    (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
    1.27     " in if ((rhs e_e) is_sqrtTerm_in v_v)                                    " ^
    1.28 -   " then (SubProblem (RootEq_',[normalize,root',univariate,equation],       " ^
    1.29 +   " then (SubProblem (RootEq',[normalize,root',univariate,equation],       " ^
    1.30     "       [no_met]) [BOOL e_e, REAL v_v])                                   " ^
    1.31 -   " else ((SubProblem (RootEq_',[univariate,equation],                      " ^
    1.32 +   " else ((SubProblem (RootEq',[univariate,equation],                      " ^
    1.33     "        [no_met]) [BOOL e_e, REAL v_v])))"
    1.34   ));
    1.35  val --------------------------------------------------+++ = "33333";
    1.36 @@ -627,9 +627,9 @@
    1.37      "  (Try (Repeat (Rewrite_Set make_rooteq                  False))) @@  " ^
    1.38      "  (Try (Rewrite_Set rooteq_simplify                       False))) e_e " ^
    1.39      " in if ((lhs e_e) is_sqrtTerm_in v_v)                                   " ^ 
    1.40 -    " then (SubProblem (RootEq_',[normalize,root',univariate,equation],      " ^
    1.41 +    " then (SubProblem (RootEq',[normalize,root',univariate,equation],      " ^
    1.42      "       [no_met]) [BOOL e_e, REAL v_v])                                " ^
    1.43 -    " else ((SubProblem (RootEq_',[univariate,equation],                    " ^
    1.44 +    " else ((SubProblem (RootEq',[univariate,equation],                    " ^
    1.45      "        [no_met]) [BOOL e_e, REAL v_v])))"
    1.46     ));
    1.47  val --------------------------------------------------++++ = "44444";

     2.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Sep 08 12:10:43 2010 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Sep 08 12:25:58 2010 +0200
     2.3 @@ -175,7 +175,7 @@
     2.4      "           (Try (Rewrite_Set rooteq_simplify   False)) @@  " ^
     2.5      "           (Try (Rewrite_Set_Inst [(bdv,v_)]               " ^
     2.6      "                                  rootrat_solve False))) e_e " ^
     2.7 -    " in (SubProblem (RootEq_,[univariate,equation],            " ^
     2.8 +    " in (SubProblem (RootEq',[univariate,equation],            " ^
     2.9      "        [no_met]) [BOOL e_e, REAL v_]))"
    2.10     ));
    2.11  calclist':= overwritel (!calclist',
wneuper/isa