src/Tools/isac/Knowledge/Biegelinie.thy
changeset 42425 da7fbace995b
parent 42411 85854c2c44d6
child 42451 bc03b5d60547
     1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Wed May 16 15:01:47 2012 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Wed May 16 15:47:22 2012 +0200
     1.3 @@ -239,7 +239,7 @@
     1.4  				        [Calc ("Atools.ident",eval_ident "#ident_"),
     1.5  				         Thm ("not_true",num_str @{thm not_true}),
     1.6  				         Thm ("not_false",num_str @{thm not_false})], 
     1.7 -				       calc = [], srls = srls, prls = Erls, crls = Atools_erls, nrls = Erls},
     1.8 +				       calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
     1.9  "Script BiegelinieScript                                                 " ^
    1.10  "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real)                  " ^
    1.11  "(r_b::bool list) (r_m::bool list) =                                     " ^
    1.12 @@ -327,7 +327,7 @@
    1.13  				        Thm ("last_thmI",num_str @{thm last_thmI}),
    1.14  				        Thm ("if_True",num_str @{thm if_True}),
    1.15  				        Thm ("if_False",num_str @{thm if_False})],
    1.16 -				     prls = Erls, crls = Atools_erls, nrls = Erls},
    1.17 +				     prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
    1.18  "Script Biegelinie2Script                                                  " ^
    1.19  "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
    1.20  "  (let                                                                    " ^
    1.21 @@ -357,7 +357,7 @@
    1.22  	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    1.23  		srls = e_rls, 
    1.24  		prls=e_rls,
    1.25 -	     crls = Atools_erls, nrls = e_rls},
    1.26 +	     crls = Atools_erls, errpats = [], nrls = e_rls},
    1.27  "empty_script"
    1.28  ));
    1.29  
    1.30 @@ -368,7 +368,7 @@
    1.31  	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    1.32  		srls = e_rls, 
    1.33  		prls=e_rls,
    1.34 -	     crls = Atools_erls, nrls = e_rls},
    1.35 +	     crls = Atools_erls, errpats = [], nrls = e_rls},
    1.36  "empty_script"
    1.37  ));
    1.38  
    1.39 @@ -379,7 +379,7 @@
    1.40  	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    1.41  		srls = e_rls, 
    1.42  		prls=e_rls,
    1.43 -	     crls = Atools_erls, nrls = e_rls},
    1.44 +	     crls = Atools_erls, errpats = [], nrls = e_rls},
    1.45  "empty_script"
    1.46  ));
    1.47  
    1.48 @@ -390,7 +390,7 @@
    1.49  	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    1.50  		srls = e_rls, 
    1.51  		prls=e_rls,
    1.52 -	     crls = Atools_erls, nrls = e_rls},
    1.53 +	     crls = Atools_erls, errpats = [], nrls = e_rls},
    1.54  "empty_script"
    1.55  ));
    1.56  
    1.57 @@ -409,7 +409,7 @@
    1.58  				      calc = [], 
    1.59  				      srls = append_rls "srls_ausBelastung" e_rls 
    1.60  				        [Calc ("Tools.rhs", eval_rhs "eval_rhs_")], 
    1.61 -				      prls = e_rls, crls = Atools_erls, nrls = e_rls},
    1.62 +				      prls = e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
    1.63  "Script Belastung2BiegelScript (q__q::real) (v_v::real) =               " ^
    1.64  "  (let q___q = Take (qq v_v = q__q);                                  " ^
    1.65  "       q___q = ((Rewrite sym_neg_equal_iff_equal True) @@              " ^
    1.66 @@ -446,7 +446,7 @@
    1.67  	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    1.68  		srls = srls2, 
    1.69  		prls=e_rls,
    1.70 -	     crls = Atools_erls, nrls = e_rls},
    1.71 +	     crls = Atools_erls, errpats = [], nrls = e_rls},
    1.72  "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
    1.73  " (let b_1 = NTH 1 r_b;                                         " ^
    1.74  "      f_s = filter_sameFunId (lhs b_1) fun_s;                   " ^
    1.75 @@ -513,7 +513,7 @@
    1.76  	      srls = append_rls "srls_in_EquationfromFunc" e_rls
    1.77  				        [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
    1.78  				         Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")], 
    1.79 -				       prls=e_rls, crls = Atools_erls, nrls = e_rls},
    1.80 +				       prls=e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
    1.81  (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
    1.82         0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
    1.83  "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^