--- a/src/HOL/Complete_Lattices.thy Sun Feb 26 20:43:33 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy Sun Feb 26 21:25:54 2012 +0100
@@ -1214,12 +1214,6 @@
less_eq (infix "\<sqsubseteq>" 50) and
less (infix "\<sqsubset>" 50)
-no_syntax (xsymbols)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
lemmas mem_simps =
insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff