avoid useless code equations
authorhaftmann
Fri Jul 03 16:51:06 2009 +0200 (2009-07-03)
changeset 31932685e7b450ab5
parent 31931 0b1d807b1c2d
child 31933 cd6511035315
avoid useless code equations
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Predicate.thy	Fri Jul 03 08:51:34 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Fri Jul 03 16:51:06 2009 +0200
     1.3 @@ -388,10 +388,10 @@
     1.4    "P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
     1.5  
     1.6  definition
     1.7 -  "\<Sqinter>A = Pred (INFI A eval)"
     1.8 +  [code del]: "\<Sqinter>A = Pred (INFI A eval)"
     1.9  
    1.10  definition
    1.11 -  "\<Squnion>A = Pred (SUPR A eval)"
    1.12 +  [code del]: "\<Squnion>A = Pred (SUPR A eval)"
    1.13  
    1.14  instance by default
    1.15    (auto simp add: less_eq_pred_def less_pred_def