src/sml/IsacKnowledge/Biegelinie.ML
changeset 3895 e5f5c5cce5a3
parent 3879 fc168b595149
     1.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML	Thu Feb 21 16:48:59 2008 +0100
     1.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML	Thu Feb 21 17:09:19 2008 +0100
     1.3 @@ -439,17 +439,6 @@
     1.4  ));
     1.5  
     1.6  store_met
     1.7 -    (prep_met Biegelinie.thy "met_equ" [] e_metID
     1.8 -	      (["Equation"],
     1.9 -	       [],
    1.10 -	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    1.11 -		srls = e_rls, 
    1.12 -		prls=e_rls,
    1.13 -	     crls = Atools_erls, nrls = e_rls},
    1.14 -"empty_script"
    1.15 -));
    1.16 -
    1.17 -store_met
    1.18      (prep_met Biegelinie.thy "met_equ_fromfun" [] e_metID
    1.19  	      (["Equation","fromFunction"],
    1.20  	       [("#Given" ,["functionEq fun_","substitution sub_"]),