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