src/Tools/isac/Knowledge/Test.thy
changeset 42424 725f0c91bbc4
parent 42314 4c05940462a0
child 42425 da7fbace995b
     1.1 --- a/src/Tools/isac/Knowledge/Test.thy	Wed May 16 08:59:09 2012 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Wed May 16 15:01:47 2012 +0200
     1.3 @@ -596,8 +596,7 @@
     1.4   (["Test"],
     1.5     [],
     1.6     {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
     1.7 -    crls=Atools_erls, nrls=e_rls(*,
     1.8 -    asm_rls=[],asm_thm=[]*)}, "empty_script"));
     1.9 +    crls=Atools_erls, nrls = e_rls}, "empty_script"));
    1.10  *}
    1.11  ML {*
    1.12  store_met
    1.13 @@ -916,7 +915,7 @@
    1.14     prls =append_rls "prls_contains_root" e_rls 
    1.15  		    [Calc ("Test.contains'_root",eval_contains_root "")],
    1.16     calc=[],
    1.17 -   crls=tval_rls, nrls=e_rls(*,asm_rls=[],
    1.18 +   crls=tval_rls, nrls = e_rls(*,asm_rls=[],
    1.19     asm_thm=[("square_equation_left",""),
    1.20  	    ("square_equation_right","")]*)},
    1.21   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
    1.22 @@ -948,7 +947,7 @@
    1.23     srls = append_rls "srls_contains_root" e_rls 
    1.24  		     [Calc ("Test.contains'_root",eval_contains_root"")],
    1.25     prls=e_rls,calc=[],
    1.26 -   crls=tval_rls, nrls=e_rls(*,asm_rls=[],
    1.27 +   crls=tval_rls, nrls = e_rls(*,asm_rls=[],
    1.28     asm_thm=[("square_equation_left",""),
    1.29  	    ("square_equation_right","")]*)},
    1.30   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
    1.31 @@ -982,7 +981,7 @@
    1.32    {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
    1.33     prls = append_rls "prls_met_test_squ_sub" e_rls
    1.34       [Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
    1.35 -   calc=[], crls=tval_rls, nrls=Test_simplify},
    1.36 +   calc=[], crls=tval_rls, nrls = Test_simplify},
    1.37    "Script Solve_root_equation (e_e::bool) (v_v::real) =       " ^
    1.38    " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@    " ^
    1.39    "            (Try (Rewrite_Set Test_simplify False))) e_e;  " ^
    1.40 @@ -1004,7 +1003,7 @@
    1.41     ("#Find"  ,["solutions v_v'i'"])
    1.42     ],
    1.43    {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
    1.44 -    crls=tval_rls, nrls=e_rls(*,
    1.45 +    crls=tval_rls, nrls = e_rls(*,
    1.46     asm_rls=[],asm_thm=[("square_equation_left",""),
    1.47  	    ("square_equation_right","")]*)},
    1.48     "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
    1.49 @@ -1027,7 +1026,7 @@
    1.50     srls = append_rls "srls_contains_root" e_rls 
    1.51  		     [Calc ("Test.contains'_root",eval_contains_root"")],
    1.52     prls=e_rls,calc=[],
    1.53 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
    1.54 +    crls=tval_rls, nrls = e_rls(*,asm_rls=[],
    1.55     asm_thm=[("square_equation_left",""),
    1.56  	    ("square_equation_right","")]*)},
    1.57   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
    1.58 @@ -1060,7 +1059,7 @@
    1.59     srls = append_rls "srls_contains_root" e_rls 
    1.60  		     [Calc ("Test.contains'_root",eval_contains_root"")],
    1.61     prls=e_rls,calc=[],
    1.62 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
    1.63 +    crls=tval_rls, nrls = e_rls(*,asm_rls=[],
    1.64     asm_thm=[("square_equation_left",""),
    1.65  	    ("square_equation_right","")]*)},
    1.66   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
    1.67 @@ -1092,7 +1091,7 @@
    1.68     srls = append_rls "srls_contains_root" e_rls 
    1.69  		     [Calc ("Test.contains'_root",eval_contains_root"")],
    1.70     prls=e_rls,calc=[],
    1.71 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
    1.72 +    crls=tval_rls, nrls = e_rls(*,asm_rls=[],
    1.73     asm_thm=[("square_equation_left",""),
    1.74  	    ("square_equation_right","")]*)},
    1.75   "Script Solve_root_equation (e_e::bool) (v_v::real)  =  " ^
    1.76 @@ -1125,7 +1124,7 @@
    1.77     srls = append_rls "srls_contains_root" e_rls 
    1.78  		     [Calc ("Test.contains'_root",eval_contains_root"")],
    1.79     prls=e_rls,calc=[],
    1.80 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],
    1.81 +    crls=tval_rls, nrls = e_rls(*,asm_rls=[],
    1.82     asm_thm=[("square_equation_left",""),
    1.83  	    ("square_equation_right","")]*)},
    1.84   "Script Solve_root_equation (e_e::bool) (v_v::real) =  " ^
    1.85 @@ -1160,7 +1159,7 @@
    1.86     ],
    1.87     {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,
    1.88      prls = assoc_rls "matches",
    1.89 -    crls=tval_rls, nrls=e_rls(*,
    1.90 +    crls=tval_rls, nrls = e_rls(*,
    1.91      asm_rls=[],asm_thm=[]*)},
    1.92    "Script Solve_plain_square (e_e::bool) (v_v::real) =           " ^
    1.93     " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@         " ^
    1.94 @@ -1183,7 +1182,7 @@
    1.95     ],
    1.96     {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,
    1.97     calc=[],
    1.98 -    crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},
    1.99 +    crls=tval_rls, nrls = e_rls},
   1.100    "Script Norm_univar_equation (e_e::bool) (v_v::real) =      " ^
   1.101     " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@   " ^
   1.102     "            (Try (Rewrite_Set Test_simplify False))) e_e   " ^