# HG changeset patch
# User haftmann
# Date 1330069776 -3600
# Node ID 0bd7c16a420024756048fde7037d07871101b8f2
# Parent  353731f11559be2861af1da0dfdee39969e878dd
explicit remove of lattice notation

diff -r 353731f11559 -r 0bd7c16a4200 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Feb 24 07:30:24 2012 +0100
+++ b/src/HOL/Relation.thy	Fri Feb 24 08:49:36 2012 +0100
@@ -931,4 +931,18 @@
   obtains "r x z"
   using assms by (auto dest: transD simp add: transp_def)
 
+no_notation
+  bot ("\<bottom>") and
+  top ("\<top>") and
+  inf (infixl "\<sqinter>" 70) and
+  sup (infixl "\<squnion>" 65) and
+  Inf ("\<Sqinter>_" [900] 900) and
+  Sup ("\<Squnion>_" [900] 900)
+
+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)
+
 end