L_LL --> L_L in scripts decompose-isar
authorWalther Neuper <neuper@ist.tugraz.at>
Tue, 13 Sep 2011 10:51:49 +0200
branchdecompose-isar
changeset 422689a4cbf65f6b8
parent 42262 31d1c917e75c
child 42269 b8a255b0ba3b
L_LL --> L_L in scripts
src/Tools/isac/Knowledge/PolyEq.thy
src/Tools/isac/Knowledge/RatEq.thy
src/Tools/isac/Knowledge/RootEq.thy
     1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Sat Sep 10 11:50:43 2011 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Tue Sep 13 10:51:49 2011 +0200
     1.3 @@ -1146,7 +1146,7 @@
     1.4      "            (Try (Rewrite_Set polyeq_simplify    False)) @@  " ^
     1.5      "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
     1.6      " (L_L::bool list) = ((Or_to_List e_e)::bool list)              " ^
     1.7 -    " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
     1.8 +    " in Check_elementwise L_L {(v_v::real). Assumptions} )"
     1.9   ));
    1.10  *}
    1.11  ML{*
    1.12 @@ -1173,7 +1173,7 @@
    1.13      "            (Try (Rewrite_Set polyeq_simplify    False)) @@  " ^
    1.14      "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
    1.15      " (L_L::bool list) = ((Or_to_List e_e)::bool list)              " ^
    1.16 -    " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
    1.17 +    " in Check_elementwise L_L {(v_v::real). Assumptions} )"
    1.18   ));
    1.19  *}
    1.20  ML{*
    1.21 @@ -1197,7 +1197,7 @@
    1.22      "            (Try (Rewrite_Set polyeq_simplify    False)) @@   " ^
    1.23      "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
    1.24      " (L_L::bool list) = ((Or_to_List e_e)::bool list)               " ^
    1.25 -    " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
    1.26 +    " in Check_elementwise L_L {(v_v::real). Assumptions} )"
    1.27   ));
    1.28  *}
    1.29  ML{*
    1.30 @@ -1245,7 +1245,7 @@
    1.31      "            (Try (Rewrite_Set polyeq_simplify     False)) @@  " ^
    1.32      "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
    1.33      " (L_L::bool list) = ((Or_to_List e_e)::bool list)               " ^
    1.34 -    " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
    1.35 +    " in Check_elementwise L_L {(v_v::real). Assumptions} )"
    1.36   ));
    1.37  *}
    1.38  ML{*
    1.39 @@ -1275,7 +1275,7 @@
    1.40      "             (Try (Rewrite_Set polyeq_simplify  False)) @@  " ^
    1.41      "             (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
    1.42      " (L_L::bool list) = ((Or_to_List e_e)::bool list)             " ^
    1.43 -    " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
    1.44 +    " in Check_elementwise L_L {(v_v::real). Assumptions} )"
    1.45     ));
    1.46  *}
    1.47  ML{*
     2.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Sat Sep 10 11:50:43 2011 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Tue Sep 13 10:51:49 2011 +0200
     2.3 @@ -214,7 +214,7 @@
     2.4      "           (Repeat(Try (Rewrite_Set RatEq_eliminate     True)))) e_e;" ^
     2.5      " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
     2.6      "                    [BOOL e_e, REAL v_v])                     " ^
     2.7 -    " in Check_elementwise L_LL {(v_v::real). Assumptions})"
     2.8 +    " in Check_elementwise L_L {(v_v::real). Assumptions})"
     2.9     ));
    2.10  *}
    2.11  
     3.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Sat Sep 10 11:50:43 2011 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Tue Sep 13 10:51:49 2011 +0200
     3.3 @@ -575,7 +575,7 @@
     3.4  "                      [no_met]) [BOOL e_e, REAL v_v])                   " ^
     3.5  "    else (SubProblem (RootEq',[univariate,equation], [no_met])         " ^
     3.6  "                     [BOOL e_e, REAL v_v]))                             " ^
     3.7 -"in Check_elementwise L_LL {(v_v::real). Assumptions})"
     3.8 +"in Check_elementwise L_L {(v_v::real). Assumptions})"
     3.9   ));
    3.10  *}
    3.11