# HG changeset patch
# User haftmann
# Date 1325963936 -3600
# Node ID 5115e47a7752bcd5957b2881bdf8d23387bd784f
# Parent  7e4a18db738492d082313e41a9cb45e6142aa74e
use Inf/Sup_bool_def/apply as code equations

diff -r 7e4a18db7384 -r 5115e47a7752 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sat Jan 07 21:19:53 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy	Sat Jan 07 20:18:56 2012 +0100
@@ -542,10 +542,10 @@
 begin
 
 definition
-  [simp]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
+  [simp, code]: "\<Sqinter>A \<longleftrightarrow> False \<notin> A"
 
 definition
-  [simp]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
+  [simp, code]: "\<Squnion>A \<longleftrightarrow> True \<in> A"
 
 instance proof
 qed (auto intro: bool_induct)
@@ -579,14 +579,14 @@
 definition
   "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
 
-lemma Inf_apply:
+lemma Inf_apply [code]:
   "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   by (simp add: Inf_fun_def)
 
 definition
   "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
 
-lemma Sup_apply:
+lemma Sup_apply [code]:
   "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   by (simp add: Sup_fun_def)