explicit remove of lattice notation
authorhaftmann
Fri, 24 Feb 2012 08:49:36 +0100
changeset 46637 0bd7c16a4200
parent 46636 353731f11559
child 46638 fc315796794e
explicit remove of lattice notation
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