# HG changeset patch
# User haftmann
# Date 1246632666 -7200
# Node ID 685e7b450ab5661d0e5c5791f0734158567395a0
# Parent  0b1d807b1c2d2e8cdf0786391e34a63ddb0cd7f0
avoid useless code equations

diff -r 0b1d807b1c2d -r 685e7b450ab5 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Jul 03 08:51:34 2009 +0200
+++ b/src/HOL/Predicate.thy	Fri Jul 03 16:51:06 2009 +0200
@@ -388,10 +388,10 @@
   "P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
 
 definition
-  "\<Sqinter>A = Pred (INFI A eval)"
+  [code del]: "\<Sqinter>A = Pred (INFI A eval)"
 
 definition
-  "\<Squnion>A = Pred (SUPR A eval)"
+  [code del]: "\<Squnion>A = Pred (SUPR A eval)"
 
 instance by default
   (auto simp add: less_eq_pred_def less_pred_def