--- a/src/HOL/Complete_Lattices.thy Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy Sun Feb 26 20:10:14 2012 +0100
@@ -8,11 +8,7 @@
notation
less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- top ("\<top>") and
- bot ("\<bottom>")
+ less (infix "\<sqsubset>" 50)
subsection {* Syntactic infimum and supremum operations *}
@@ -23,6 +19,7 @@
class Sup =
fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
+
subsection {* Abstract complete lattices *}
class complete_lattice = bounded_lattice + Inf + Sup +
@@ -1214,14 +1211,8 @@
text {* Finally *}
no_notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- 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)
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50)
no_syntax (xsymbols)
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
--- a/src/HOL/Lattices.thy Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Lattices.thy Sun Feb 26 20:10:14 2012 +0100
@@ -43,13 +43,7 @@
end
-subsection {* Concrete lattices *}
-
-notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- bot ("\<bottom>") and
- top ("\<top>")
+subsection {* Syntactic infimum and supremum operations *}
class inf =
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -57,6 +51,13 @@
class sup =
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+
+subsection {* Concrete lattices *}
+
+notation
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50)
+
class semilattice_inf = order + inf +
assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
@@ -759,12 +760,8 @@
no_notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- top ("\<top>") and
- bot ("\<bottom>")
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50)
end
--- a/src/HOL/Orderings.thy Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Orderings.thy Sun Feb 26 20:10:14 2012 +0100
@@ -1426,8 +1426,4 @@
lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
-no_notation
- top ("\<top>") and
- bot ("\<bottom>")
-
end
--- a/src/HOL/Plain.thy Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Plain.thy Sun Feb 26 20:10:14 2012 +0100
@@ -9,4 +9,18 @@
include @{text Hilbert_Choice}.
*}
+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
--- a/src/HOL/Relation.thy Sun Feb 26 20:08:12 2012 +0100
+++ b/src/HOL/Relation.thy Sun Feb 26 20:10:14 2012 +0100
@@ -939,19 +939,5 @@
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