# HG changeset patch
# User haftmann
# Date 1473242349 -7200
# Node ID 9f004fbf9d5c25034d3adc683d8d8991ba5387aa
# Parent  58f74e90b96d07f6b1f01061faf4825b68d2cfe5
discontinued theory-local special syntax for lattice orderings

diff -r 58f74e90b96d -r 9f004fbf9d5c src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Wed Sep 07 11:59:07 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy	Wed Sep 07 11:59:09 2016 +0200
@@ -11,11 +11,6 @@
   imports Fun
 begin
 
-notation
-  less_eq (infix "\<sqsubseteq>" 50) and
-  less (infix "\<sqsubset>" 50)
-
-
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class Inf =
@@ -116,10 +111,10 @@
 in terms of infimum and supremum.\<close>
 
 class complete_lattice = lattice + Inf + Sup + bot + top +
-  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
-    and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
-    and Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
-    and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
+  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
+    and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
+    and Sup_upper: "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
+    and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
     and Inf_empty [simp]: "\<Sqinter>{} = \<top>"
     and Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
 begin
@@ -158,40 +153,40 @@
   "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (\<Sqinter>i\<in>A. f i) = x"
   using Inf_eqI [of "f ` A" x] by auto
 
-lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
+lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> f i"
   using Inf_lower [of _ "f ` A"] by simp
 
-lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
+lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (\<Sqinter>i\<in>A. f i)"
   using Inf_greatest [of "f ` A"] by auto
 
-lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<le> (\<Squnion>i\<in>A. f i)"
   using Sup_upper [of _ "f ` A"] by simp
 
-lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
+lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<le> u"
   using Sup_least [of "f ` A"] by auto
 
-lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
+lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> \<Sqinter>A \<le> v"
   using Inf_lower [of u A] by auto
 
-lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
+lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<le> u"
   using INF_lower [of i A f] by auto
 
-lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
+lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> \<Squnion>A"
   using Sup_upper [of u A] by auto
 
-lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (\<Squnion>i\<in>A. f i)"
   using SUP_upper [of i A f] by auto
 
-lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
+lemma le_Inf_iff: "b \<le> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)"
   by (auto intro: Inf_greatest dest: Inf_lower)
 
-lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
+lemma le_INF_iff: "u \<le> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
   using le_Inf_iff [of _ "f ` A"] by simp
 
-lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
+lemma Sup_le_iff: "\<Squnion>A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)"
   by (auto intro: Sup_least dest: Sup_upper)
 
-lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
+lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
   using Sup_le_iff [of "f ` A"] by simp
 
 lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
@@ -218,68 +213,68 @@
 lemma Sup_UNIV [simp]: "\<Squnion>UNIV = \<top>"
   by (auto intro!: antisym Sup_upper)
 
-lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
 
-lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
+lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
   by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
 
-lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
+lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<le> \<Sqinter>B"
   by (auto intro: Inf_greatest Inf_lower)
 
-lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
+lemma Sup_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<le> \<Squnion>B"
   by (auto intro: Sup_least Sup_upper)
 
 lemma Inf_mono:
-  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
-  shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
+  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
+  shows "\<Sqinter>A \<le> \<Sqinter>B"
 proof (rule Inf_greatest)
   fix b assume "b \<in> B"
-  with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
-  from \<open>a \<in> A\<close> have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
-  with \<open>a \<sqsubseteq> b\<close> show "\<Sqinter>A \<sqsubseteq> b" by auto
+  with assms obtain a where "a \<in> A" and "a \<le> b" by blast
+  from \<open>a \<in> A\<close> have "\<Sqinter>A \<le> a" by (rule Inf_lower)
+  with \<open>a \<le> b\<close> show "\<Sqinter>A \<le> b" by auto
 qed
 
-lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
+lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<le> (\<Sqinter>n\<in>B. g n)"
   using Inf_mono [of "g ` B" "f ` A"] by auto
 
 lemma Sup_mono:
-  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
-  shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
+  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
+  shows "\<Squnion>A \<le> \<Squnion>B"
 proof (rule Sup_least)
   fix a assume "a \<in> A"
-  with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
-  from \<open>b \<in> B\<close> have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
-  with \<open>a \<sqsubseteq> b\<close> show "a \<sqsubseteq> \<Squnion>B" by auto
+  with assms obtain b where "b \<in> B" and "a \<le> b" by blast
+  from \<open>b \<in> B\<close> have "b \<le> \<Squnion>B" by (rule Sup_upper)
+  with \<open>a \<le> b\<close> show "a \<le> \<Squnion>B" by auto
 qed
 
-lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
+lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<le> (\<Squnion>n\<in>B. g n)"
   using Sup_mono [of "f ` A" "g ` B"] by auto
 
-lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
+lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>B. g x)"
   \<comment> \<open>The last inclusion is POSITIVE!\<close>
   by (blast intro: INF_mono dest: subsetD)
 
-lemma SUP_subset_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
+lemma SUP_subset_mono: "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> (\<Squnion>x\<in>B. g x)"
   by (blast intro: SUP_mono dest: subsetD)
 
 lemma Inf_less_eq:
-  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
+  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<le> u"
     and "A \<noteq> {}"
-  shows "\<Sqinter>A \<sqsubseteq> u"
+  shows "\<Sqinter>A \<le> u"
 proof -
   from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
-  moreover from \<open>v \<in> A\<close> assms(1) have "v \<sqsubseteq> u" by blast
+  moreover from \<open>v \<in> A\<close> assms(1) have "v \<le> u" by blast
   ultimately show ?thesis by (rule Inf_lower2)
 qed
 
 lemma less_eq_Sup:
-  assumes "\<And>v. v \<in> A \<Longrightarrow> u \<sqsubseteq> v"
+  assumes "\<And>v. v \<in> A \<Longrightarrow> u \<le> v"
     and "A \<noteq> {}"
-  shows "u \<sqsubseteq> \<Squnion>A"
+  shows "u \<le> \<Squnion>A"
 proof -
   from \<open>A \<noteq> {}\<close> obtain v where "v \<in> A" by blast
-  moreover from \<open>v \<in> A\<close> assms(1) have "u \<sqsubseteq> v" by blast
+  moreover from \<open>v \<in> A\<close> assms(1) have "u \<le> v" by blast
   ultimately show ?thesis by (rule Sup_upper2)
 qed
 
@@ -295,10 +290,10 @@
   shows "SUPREMUM A f = SUPREMUM B g"
   by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
 
-lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
+lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)"
   by (auto intro: Inf_greatest Inf_lower)
 
-lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<sqsubseteq> \<Squnion>A \<sqinter> \<Squnion>B "
+lemma Sup_inter_less_eq: "\<Squnion>(A \<inter> B) \<le> \<Squnion>A \<sqinter> \<Squnion>B "
   by (auto intro: Sup_least Sup_upper)
 
 lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
@@ -574,16 +569,16 @@
 lemma complete_linorder_sup_max: "sup = max"
   by (auto intro: antisym simp add: max_def fun_eq_iff)
 
-lemma Inf_less_iff: "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
+lemma Inf_less_iff: "\<Sqinter>S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
   by (simp add: not_le [symmetric] le_Inf_iff)
 
-lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
+lemma INF_less_iff: "(\<Sqinter>i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
   by (simp add: Inf_less_iff [of "f ` A"])
 
-lemma less_Sup_iff: "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
+lemma less_Sup_iff: "a < \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
   by (simp add: not_le [symmetric] Sup_le_iff)
 
-lemma less_SUP_iff: "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
+lemma less_SUP_iff: "a < (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
   by (simp add: less_Sup_iff [of _ "f ` A"])
 
 lemma Sup_eq_top_iff [simp]: "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
@@ -1426,10 +1421,6 @@
 
 text \<open>Finally\<close>
 
-no_notation
-  less_eq (infix "\<sqsubseteq>" 50) and
-  less (infix "\<sqsubset>" 50)
-
 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
diff -r 58f74e90b96d -r 9f004fbf9d5c src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Sep 07 11:59:07 2016 +0200
+++ b/src/HOL/Lattices.thy	Wed Sep 07 11:59:09 2016 +0200
@@ -161,19 +161,15 @@
 
 subsection \<open>Concrete lattices\<close>
 
-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"
-  and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
+  assumes inf_le1 [simp]: "x \<sqinter> y \<le> x"
+  and inf_le2 [simp]: "x \<sqinter> y \<le> y"
+  and inf_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
 
 class semilattice_sup = order + sup +
-  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
-  and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
-  and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
+  assumes sup_ge1 [simp]: "x \<le> x \<squnion> y"
+  and sup_ge2 [simp]: "y \<le> x \<squnion> y"
+  and sup_least: "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
 begin
 
 text \<open>Dual lattice.\<close>
@@ -191,28 +187,28 @@
 context semilattice_inf
 begin
 
-lemma le_infI1: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+lemma le_infI1: "a \<le> x \<Longrightarrow> a \<sqinter> b \<le> x"
   by (rule order_trans) auto
 
-lemma le_infI2: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+lemma le_infI2: "b \<le> x \<Longrightarrow> a \<sqinter> b \<le> x"
   by (rule order_trans) auto
 
-lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
+lemma le_infI: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> a \<sqinter> b"
   by (fact inf_greatest) (* FIXME: duplicate lemma *)
 
-lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+lemma le_infE: "x \<le> a \<sqinter> b \<Longrightarrow> (x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> P) \<Longrightarrow> P"
   by (blast intro: order_trans inf_le1 inf_le2)
 
-lemma le_inf_iff: "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
+lemma le_inf_iff: "x \<le> y \<sqinter> z \<longleftrightarrow> x \<le> y \<and> x \<le> z"
   by (blast intro: le_infI elim: le_infE)
 
-lemma le_iff_inf: "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
+lemma le_iff_inf: "x \<le> y \<longleftrightarrow> x \<sqinter> y = x"
   by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff)
 
-lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
+lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d"
   by (fast intro: inf_greatest le_infI1 le_infI2)
 
-lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
+lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
   by (auto simp add: mono_def intro: Lattices.inf_greatest)
 
 end
@@ -220,28 +216,28 @@
 context semilattice_sup
 begin
 
-lemma le_supI1: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI1: "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b"
   by (rule order_trans) auto
 
-lemma le_supI2: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI2: "x \<le> b \<Longrightarrow> x \<le> a \<squnion> b"
   by (rule order_trans) auto
 
-lemma le_supI: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
+lemma le_supI: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> a \<squnion> b \<le> x"
   by (fact sup_least) (* FIXME: duplicate lemma *)
 
-lemma le_supE: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
+lemma le_supE: "a \<squnion> b \<le> x \<Longrightarrow> (a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
   by (blast intro: order_trans sup_ge1 sup_ge2)
 
-lemma le_sup_iff: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
+lemma le_sup_iff: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
   by (blast intro: le_supI elim: le_supE)
 
-lemma le_iff_sup: "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
+lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y"
   by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff)
 
-lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
+lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d"
   by (fast intro: sup_least le_supI1 le_supI2)
 
-lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
+lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
   by (auto simp add: mono_def intro: Lattices.sup_least)
 
 end
@@ -284,10 +280,10 @@
 lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"
   by (fact inf.right_idem) (* already simp *)
 
-lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+lemma inf_absorb1: "x \<le> y \<Longrightarrow> x \<sqinter> y = x"
   by (rule antisym) auto
 
-lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+lemma inf_absorb2: "y \<le> x \<Longrightarrow> x \<sqinter> y = y"
   by (rule antisym) auto
 
 lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
@@ -326,10 +322,10 @@
 lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   by (fact sup.left_idem)
 
-lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+lemma sup_absorb1: "y \<le> x \<Longrightarrow> x \<squnion> y = x"
   by (rule antisym) auto
 
-lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+lemma sup_absorb2: "x \<le> y \<Longrightarrow> x \<squnion> y = y"
   by (rule antisym) auto
 
 lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
@@ -358,10 +354,10 @@
 
 text \<open>Towards distributivity.\<close>
 
-lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
+lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<le> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
-lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
+lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<le> x \<sqinter> (y \<squnion> z)"
   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
 text \<open>If you have one of them, you have them all.\<close>
@@ -402,10 +398,10 @@
 context semilattice_inf
 begin
 
-lemma less_infI1: "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
+lemma less_infI1: "a < x \<Longrightarrow> a \<sqinter> b < x"
   by (auto simp add: less_le inf_absorb1 intro: le_infI1)
 
-lemma less_infI2: "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
+lemma less_infI2: "b < x \<Longrightarrow> a \<sqinter> b < x"
   by (auto simp add: less_le inf_absorb2 intro: le_infI2)
 
 end
@@ -413,11 +409,11 @@
 context semilattice_sup
 begin
 
-lemma less_supI1: "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
+lemma less_supI1: "x < a \<Longrightarrow> x < a \<squnion> b"
   using dual_semilattice
   by (rule semilattice_inf.less_infI1)
 
-lemma less_supI2: "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
+lemma less_supI2: "x < b \<Longrightarrow> x < a \<squnion> b"
   using dual_semilattice
   by (rule semilattice_inf.less_infI2)
 
@@ -616,8 +612,8 @@
   by (rule boolean_algebra.compl_inf)
 
 lemma compl_mono:
-  assumes "x \<sqsubseteq> y"
-  shows "- y \<sqsubseteq> - x"
+  assumes "x \<le> y"
+  shows "- y \<le> - x"
 proof -
   from assms have "x \<squnion> y = y" by (simp only: le_iff_sup)
   then have "- (x \<squnion> y) = - y" by simp
@@ -626,41 +622,41 @@
   then show ?thesis by (simp only: le_iff_inf)
 qed
 
-lemma compl_le_compl_iff [simp]: "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
+lemma compl_le_compl_iff [simp]: "- x \<le> - y \<longleftrightarrow> y \<le> x"
   by (auto dest: compl_mono)
 
 lemma compl_le_swap1:
-  assumes "y \<sqsubseteq> - x"
-  shows "x \<sqsubseteq> -y"
+  assumes "y \<le> - x"
+  shows "x \<le> -y"
 proof -
-  from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
+  from assms have "- (- x) \<le> - y" by (simp only: compl_le_compl_iff)
   then show ?thesis by simp
 qed
 
 lemma compl_le_swap2:
-  assumes "- y \<sqsubseteq> x"
-  shows "- x \<sqsubseteq> y"
+  assumes "- y \<le> x"
+  shows "- x \<le> y"
 proof -
-  from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
+  from assms have "- x \<le> - (- y)" by (simp only: compl_le_compl_iff)
   then show ?thesis by simp
 qed
 
-lemma compl_less_compl_iff: "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"  (* TODO: declare [simp] ? *)
+lemma compl_less_compl_iff: "- x < - y \<longleftrightarrow> y < x"  (* TODO: declare [simp] ? *)
   by (auto simp add: less_le)
 
 lemma compl_less_swap1:
-  assumes "y \<sqsubset> - x"
-  shows "x \<sqsubset> - y"
+  assumes "y < - x"
+  shows "x < - y"
 proof -
-  from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
+  from assms have "- (- x) < - y" by (simp only: compl_less_compl_iff)
   then show ?thesis by simp
 qed
 
 lemma compl_less_swap2:
-  assumes "- y \<sqsubset> x"
-  shows "- x \<sqsubset> y"
+  assumes "- y < x"
+  shows "- x < y"
 proof -
-  from assms have "- x \<sqsubset> - (- y)"
+  from assms have "- x < - (- y)"
     by (simp only: compl_less_compl_iff)
   then show ?thesis by simp
 qed
@@ -772,31 +768,31 @@
 
 lemma (in semilattice_inf) inf_unique:
   fixes f  (infixl "\<triangle>" 70)
-  assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x"
-    and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
-    and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
+  assumes le1: "\<And>x y. x \<triangle> y \<le> x"
+    and le2: "\<And>x y. x \<triangle> y \<le> y"
+    and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
   shows "x \<sqinter> y = x \<triangle> y"
 proof (rule antisym)
-  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y"
+  show "x \<triangle> y \<le> x \<sqinter> y"
     by (rule le_infI) (rule le1, rule le2)
-  have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
+  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
     by (blast intro: greatest)
-  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y"
+  show "x \<sqinter> y \<le> x \<triangle> y"
     by (rule leI) simp_all
 qed
 
 lemma (in semilattice_sup) sup_unique:
   fixes f  (infixl "\<nabla>" 70)
-  assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y"
-    and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
-    and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
+  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y"
+    and ge2: "\<And>x y. y \<le> x \<nabla> y"
+    and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
   shows "x \<squnion> y = x \<nabla> y"
 proof (rule antisym)
-  show "x \<squnion> y \<sqsubseteq> x \<nabla> y"
+  show "x \<squnion> y \<le> x \<nabla> y"
     by (rule le_supI) (rule ge1, rule ge2)
-  have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z"
+  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z"
     by (blast intro: least)
-  show "x \<nabla> y \<sqsubseteq> x \<squnion> y"
+  show "x \<nabla> y \<le> x \<squnion> y"
     by (rule leI) simp_all
 qed
 
@@ -942,9 +938,4 @@
 lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   by (auto simp add: sup_fun_def)
 
-
-no_notation
-  less_eq (infix "\<sqsubseteq>" 50) and
-  less (infix "\<sqsubset>" 50)
-
 end