# HG changeset patch
# User haftmann
# Date 1330287954 -3600
# Node ID 78bada13da4637480a92e44e7f8e5543d518e966
# Parent  1f8b766224f6566525213b71f22c852019e433b7
retain syntax here

diff -r 1f8b766224f6 -r 78bada13da46 src/HOL/Complete_Lattices.thy
--- 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