proper syntax during class specification

--- a/src/HOL/Dense_Linear_Order.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -22,153 +22,153 @@
 context linorder
 begin
 
-lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear)
+lemma less_not_permute: "\<not> (x \<^loc>< y \<and> y \<^loc>< x)" by (simp add: not_less linear)
 
 lemma gather_simps: 
   shows 
-  "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> x \<sqsubset> u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> (insert u U). x \<sqsubset> y) \<and> P x)"
-  and "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> l \<sqsubset> x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> P x)"
-  "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> x \<sqsubset> u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> (insert u U). x \<sqsubset> y))"
-  and "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> l \<sqsubset> x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y))"  by auto
+  "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> x \<^loc>< u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> (insert u U). x \<^loc>< y) \<and> P x)"
+  and "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> l \<^loc>< x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> P x)"
+  "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> x \<^loc>< u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> (insert u U). x \<^loc>< y))"
+  and "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y) \<and> l \<^loc>< x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y))"  by auto
 
 lemma 
-  gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y\<in> {}. x \<sqsubset> y) \<and> P x)" 
+  gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y\<in> {}. x \<^loc>< y) \<and> P x)" 
   by simp
 
-text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
-lemma minf_lt:  "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubset> t \<longleftrightarrow> True)" by auto
-lemma minf_gt: "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow>  (t \<sqsubset> x \<longleftrightarrow>  False)"
+text{* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
+lemma minf_lt:  "\<exists>z . \<forall>x. x \<^loc>< z \<longrightarrow> (x \<^loc>< t \<longleftrightarrow> True)" by auto
+lemma minf_gt: "\<exists>z . \<forall>x. x \<^loc>< z \<longrightarrow>  (t \<^loc>< x \<longleftrightarrow>  False)"
   by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
 
-lemma minf_le: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubseteq> t \<longleftrightarrow> True)" by (auto simp add: less_le)
-lemma minf_ge: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (t \<sqsubseteq> x \<longleftrightarrow> False)"
+lemma minf_le: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x \<^loc>\<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma minf_ge: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (t \<^loc>\<le> x \<longleftrightarrow> False)"
   by (auto simp add: less_le not_less not_le)
-lemma minf_eq: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma minf_neq: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma minf_P: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma minf_eq: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma minf_neq: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma minf_P: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
 
-text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
-lemma pinf_gt:  "\<exists>z . \<forall>x. z \<sqsubset> x \<longrightarrow> (t \<sqsubset> x \<longleftrightarrow> True)" by auto
-lemma pinf_lt: "\<exists>z . \<forall>x. z \<sqsubset> x \<longrightarrow>  (x \<sqsubset> t \<longleftrightarrow>  False)"
+text{* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
+lemma pinf_gt:  "\<exists>z . \<forall>x. z \<^loc>< x \<longrightarrow> (t \<^loc>< x \<longleftrightarrow> True)" by auto
+lemma pinf_lt: "\<exists>z . \<forall>x. z \<^loc>< x \<longrightarrow>  (x \<^loc>< t \<longleftrightarrow>  False)"
   by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
 
-lemma pinf_ge: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (t \<sqsubseteq> x \<longleftrightarrow> True)" by (auto simp add: less_le)
-lemma pinf_le: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x \<sqsubseteq> t \<longleftrightarrow> False)"
+lemma pinf_ge: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (t \<^loc>\<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma pinf_le: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x \<^loc>\<le> t \<longleftrightarrow> False)"
   by (auto simp add: less_le not_less not_le)
-lemma pinf_eq: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma pinf_neq: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma pinf_P: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma pinf_eq: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma pinf_neq: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma pinf_P: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
 
-lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<sqsubset> t \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
-lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t \<sqsubset> x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)"
+lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<^loc>< t \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
+lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t \<^loc>< x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)"
   by (auto simp add: le_less)
-lemma  nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<sqsubseteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
-lemma  nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<sqsubseteq> x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
-lemma  nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
-lemma  nmi_neq: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
-lemma  nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
-lemma  nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x) ;
-  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)\<rbrakk> \<Longrightarrow>
-  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
-lemma  nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x) ;
-  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)\<rbrakk> \<Longrightarrow>
-  \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
+lemma  nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<^loc>\<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
+lemma  nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<^loc>\<le> x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
+lemma  nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
+lemma  nmi_neq: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
+lemma  nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
+lemma  nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x) ;
+  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)\<rbrakk> \<Longrightarrow>
+  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
+lemma  nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x) ;
+  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)\<rbrakk> \<Longrightarrow>
+  \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
 
-lemma  npi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<sqsubset> t \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by (auto simp add: le_less)
-lemma  npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<sqsubset> x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
-lemma  npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<sqsubseteq> t \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
-lemma  npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<sqsubseteq> x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
-lemma  npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
-lemma  npi_neq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u )" by auto
-lemma  npi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
-lemma  npi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u) ;  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk>
-  \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
-lemma  npi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk>
-  \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
+lemma  npi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<^loc>< t \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by (auto simp add: le_less)
+lemma  npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<^loc>< x \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
+lemma  npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<^loc>\<le> t \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
+lemma  npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<^loc>\<le> x \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
+lemma  npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
+lemma  npi_neq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u )" by auto
+lemma  npi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
+lemma  npi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u) ;  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)\<rbrakk>
+  \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
+lemma  npi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)\<rbrakk>
+  \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
 
-lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> x \<sqsubset> t \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y \<sqsubset> t)"
+lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x \<^loc>< t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y \<^loc>< t)"
 proof(clarsimp)
-  fix x l u y  assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x"
-    and xu: "x\<sqsubset>u"  and px: "x \<sqsubset> t" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
+  fix x l u y  assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x"
+    and xu: "x\<^loc><u"  and px: "x \<^loc>< t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
   from tU noU ly yu have tny: "t\<noteq>y" by auto
-  {assume H: "t \<sqsubset> y"
+  {assume H: "t \<^loc>< y"
     from less_trans[OF lx px] less_trans[OF H yu]
-    have "l \<sqsubset> t \<and> t \<sqsubset> u"  by simp
+    have "l \<^loc>< t \<and> t \<^loc>< u"  by simp
     with tU noU have "False" by auto}
-  hence "\<not> t \<sqsubset> y"  by auto hence "y \<sqsubseteq> t" by (simp add: not_less)
-  thus "y \<sqsubset> t" using tny by (simp add: less_le)
+  hence "\<not> t \<^loc>< y"  by auto hence "y \<^loc>\<le> t" by (simp add: not_less)
+  thus "y \<^loc>< t" using tny by (simp add: less_le)
 qed
 
-lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l \<sqsubset> x \<and> x \<sqsubset> u \<and> t \<sqsubset> x \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> t \<sqsubset> y)"
+lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l \<^loc>< x \<and> x \<^loc>< u \<and> t \<^loc>< x \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> t \<^loc>< y)"
 proof(clarsimp)
   fix x l u y
-  assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x" and xu: "x\<sqsubset>u"
-  and px: "t \<sqsubset> x" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
+  assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" and xu: "x\<^loc><u"
+  and px: "t \<^loc>< x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
   from tU noU ly yu have tny: "t\<noteq>y" by auto
-  {assume H: "y\<sqsubset> t"
-    from less_trans[OF ly H] less_trans[OF px xu] have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
+  {assume H: "y\<^loc>< t"
+    from less_trans[OF ly H] less_trans[OF px xu] have "l \<^loc>< t \<and> t \<^loc>< u" by simp
     with tU noU have "False" by auto}
-  hence "\<not> y\<sqsubset>t"  by auto hence "t \<sqsubseteq> y" by (auto simp add: not_less)
-  thus "t \<sqsubset> y" using tny by (simp add:less_le)
+  hence "\<not> y\<^loc><t"  by auto hence "t \<^loc>\<le> y" by (auto simp add: not_less)
+  thus "t \<^loc>< y" using tny by (simp add:less_le)
 qed
 
-lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> x \<sqsubseteq> t \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y\<sqsubseteq> t)"
+lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x \<^loc>\<le> t \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y\<^loc>\<le> t)"
 proof(clarsimp)
   fix x l u y
-  assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x" and xu: "x\<sqsubset>u"
-  and px: "x \<sqsubseteq> t" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
+  assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" and xu: "x\<^loc><u"
+  and px: "x \<^loc>\<le> t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
   from tU noU ly yu have tny: "t\<noteq>y" by auto
-  {assume H: "t \<sqsubset> y"
+  {assume H: "t \<^loc>< y"
     from less_le_trans[OF lx px] less_trans[OF H yu]
-    have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
+    have "l \<^loc>< t \<and> t \<^loc>< u" by simp
     with tU noU have "False" by auto}
-  hence "\<not> t \<sqsubset> y"  by auto thus "y \<sqsubseteq> t" by (simp add: not_less)
+  hence "\<not> t \<^loc>< y"  by auto thus "y \<^loc>\<le> t" by (simp add: not_less)
 qed
 
-lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> t \<sqsubseteq> x \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> t \<sqsubseteq> y)"
+lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> t \<^loc>\<le> x \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> t \<^loc>\<le> y)"
 proof(clarsimp)
   fix x l u y
-  assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x" and xu: "x\<sqsubset>u"
-  and px: "t \<sqsubseteq> x" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
+  assume tU: "t \<in> U" and noU: "\<forall>t. l \<^loc>< t \<and> t \<^loc>< u \<longrightarrow> t \<notin> U" and lx: "l \<^loc>< x" and xu: "x\<^loc><u"
+  and px: "t \<^loc>\<le> x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
   from tU noU ly yu have tny: "t\<noteq>y" by auto
-  {assume H: "y\<sqsubset> t"
+  {assume H: "y\<^loc>< t"
     from less_trans[OF ly H] le_less_trans[OF px xu]
-    have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
+    have "l \<^loc>< t \<and> t \<^loc>< u" by simp
     with tU noU have "False" by auto}
-  hence "\<not> y\<sqsubset>t"  by auto thus "t \<sqsubseteq> y" by (simp add: not_less)
+  hence "\<not> y\<^loc><t"  by auto thus "t \<^loc>\<le> y" by (simp add: not_less)
 qed
-lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> x = t   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y= t)"  by auto
-lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> x \<noteq> t   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y\<noteq> t)"  by auto
-lemma lin_dense_P: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P)"  by auto
+lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x = t   \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y= t)"  by auto
+lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> x \<noteq> t   \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> y\<noteq> t)"  by auto
+lemma lin_dense_P: "\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P   \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P)"  by auto
 
 lemma lin_dense_conj:
-  "\<lbrakk>\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P1 x
-  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P1 y) ;
-  \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P2 x
-  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
-  \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> (P1 x \<and> P2 x)
-  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> (P1 y \<and> P2 y))"
+  "\<lbrakk>\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P1 x
+  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ;
+  \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P2 x
+  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
+  \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> (P1 x \<and> P2 x)
+  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<and> P2 y))"
   by blast
 lemma lin_dense_disj:
-  "\<lbrakk>\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P1 x
-  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P1 y) ;
-  \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P2 x
-  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
-  \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> (P1 x \<or> P2 x)
-  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> (P1 y \<or> P2 y))"
+  "\<lbrakk>\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P1 x
+  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ;
+  \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P2 x
+  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
+  \<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> (P1 x \<or> P2 x)
+  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<or> P2 y))"
   by blast
 
-lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk>
-  \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')"
+lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)\<rbrakk>
+  \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u')"
 by auto
 
 lemma finite_set_intervals:
-  assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S"
-  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<sqsubseteq> x" and Su: "\<forall> x\<in> S. x \<sqsubseteq> u"
-  shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S) \<and> a \<sqsubseteq> x \<and> x \<sqsubseteq> b \<and> P x"
+  assumes px: "P x" and lx: "l \<^loc>\<le> x" and xu: "x \<^loc>\<le> u" and linS: "l\<in> S"
+  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<^loc>\<le> x" and Su: "\<forall> x\<in> S. x \<^loc>\<le> u"
+  shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S) \<and> a \<^loc>\<le> x \<and> x \<^loc>\<le> b \<and> P x"
 proof-
-  let ?Mx = "{y. y\<in> S \<and> y \<sqsubseteq> x}"
-  let ?xM = "{y. y\<in> S \<and> x \<sqsubseteq> y}"
+  let ?Mx = "{y. y\<in> S \<and> y \<^loc>\<le> x}"
+  let ?xM = "{y. y\<in> S \<and> x \<^loc>\<le> y}"
   let ?a = "Max ?Mx"
   let ?b = "Min ?xM"
   have MxS: "?Mx \<subseteq> S" by blast
@@ -179,31 +179,31 @@
   hence fxM: "finite ?xM" using fS finite_subset by auto
   from xu uinS have linxM: "u \<in> ?xM" by blast
   hence xMne: "?xM \<noteq> {}" by blast
-  have ax:"?a \<sqsubseteq> x" using Mxne fMx by auto
-  have xb:"x \<sqsubseteq> ?b" using xMne fxM by auto
+  have ax:"?a \<^loc>\<le> x" using Mxne fMx by auto
+  have xb:"x \<^loc>\<le> ?b" using xMne fxM by auto
   have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
   have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
-  have noy:"\<forall> y. ?a \<sqsubset> y \<and> y \<sqsubset> ?b \<longrightarrow> y \<notin> S"
+  have noy:"\<forall> y. ?a \<^loc>< y \<and> y \<^loc>< ?b \<longrightarrow> y \<notin> S"
   proof(clarsimp)
-    fix y   assume ay: "?a \<sqsubset> y" and yb: "y \<sqsubset> ?b" and yS: "y \<in> S"
+    fix y   assume ay: "?a \<^loc>< y" and yb: "y \<^loc>< ?b" and yS: "y \<in> S"
     from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear)
-    moreover {assume "y \<in> ?Mx" hence "y \<sqsubseteq> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])}
-    moreover {assume "y \<in> ?xM" hence "?b \<sqsubseteq> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])}
+    moreover {assume "y \<in> ?Mx" hence "y \<^loc>\<le> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])}
+    moreover {assume "y \<in> ?xM" hence "?b \<^loc>\<le> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])}
     ultimately show "False" by blast
   qed
   from ainS binS noy ax xb px show ?thesis by blast
 qed
 
 lemma finite_set_intervals2:
-  assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S"
-  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<sqsubseteq> x" and Su: "\<forall> x\<in> S. x \<sqsubseteq> u"
-  shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S) \<and> a \<sqsubset> x \<and> x \<sqsubset> b \<and> P x)"
+  assumes px: "P x" and lx: "l \<^loc>\<le> x" and xu: "x \<^loc>\<le> u" and linS: "l\<in> S"
+  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<^loc>\<le> x" and Su: "\<forall> x\<in> S. x \<^loc>\<le> u"
+  shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S) \<and> a \<^loc>< x \<and> x \<^loc>< b \<and> P x)"
 proof-
   from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
   obtain a and b where
-    as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S"
-    and axb: "a \<sqsubseteq> x \<and> x \<sqsubseteq> b \<and> P x"  by auto
-  from axb have "x= a \<or> x= b \<or> (a \<sqsubset> x \<and> x \<sqsubset> b)" by (auto simp add: le_less)
+    as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S"
+    and axb: "a \<^loc>\<le> x \<and> x \<^loc>\<le> b \<and> P x"  by auto
+  from axb have "x= a \<or> x= b \<or> (a \<^loc>< x \<and> x \<^loc>< b)" by (auto simp add: le_less)
   thus ?thesis using px as bs noS by blast
 qed
 
@@ -216,44 +216,44 @@
 
 lemma dlo_qe_bnds: 
   assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
-  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<sqsubset> u)"
+  shows "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<^loc>< u)"
 proof (simp only: atomize_eq, rule iffI)
   assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
   then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
   {fix l u assume l: "l \<in> L" and u: "u \<in> U"
     from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
-    have "l \<sqsubset> u" .}
+    have "l \<^loc>< u" .}
   thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
 next
   assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
   let ?ML = "Max L"
   let ?MU = "Min U"  
-  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto
-  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
-  from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
-  with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
-  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" by auto
-  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" by auto
+  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<^loc>\<le> ?ML" by auto
+  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<^loc>\<le> u" by auto
+  from th1 th2 H have "?ML \<^loc>< ?MU" by auto
+  with dense obtain w where th3: "?ML \<^loc>< w" and th4: "w \<^loc>< ?MU" by blast
+  from th3 th1' have "\<forall>l \<in> L. l \<^loc>< w" by auto
+  moreover from th4 th2' have "\<forall>u \<in> U. w \<^loc>< u" by auto
   ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
 qed
 
 lemma dlo_qe_noub: 
   assumes ne: "L \<noteq> {}" and fL: "finite L"
-  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True"
+  shows "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> {}. x \<^loc>< y)) \<equiv> True"
 proof(simp add: atomize_eq)
-  from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast
-  from ne fL have "\<forall>x \<in> L. x \<sqsubseteq> Max L" by simp
-  with M have "\<forall>x\<in>L. x \<sqsubset> M" by (auto intro: le_less_trans)
+  from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<^loc>< M" by blast
+  from ne fL have "\<forall>x \<in> L. x \<^loc>\<le> Max L" by simp
+  with M have "\<forall>x\<in>L. x \<^loc>< M" by (auto intro: le_less_trans)
   thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
 qed
 
 lemma dlo_qe_nolb: 
   assumes ne: "U \<noteq> {}" and fU: "finite U"
-  shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True"
+  shows "(\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> True"
 proof(simp add: atomize_eq)
-  from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast
-  from ne fU have "\<forall>x \<in> U. Min U \<sqsubseteq> x" by simp
-  with M have "\<forall>x\<in>U. M \<sqsubset> x" by (auto intro: less_le_trans)
+  from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<^loc>< Min U" by blast
+  from ne fU have "\<forall>x \<in> U. Min U \<^loc>\<le> x" by simp
+  with M have "\<forall>x\<in>U. M \<^loc>< x" by (auto intro: less_le_trans)
   thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
 qed
 
@@ -263,9 +263,12 @@
 lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
   le_less neq_iff linear less_not_permute
 
-lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" .
-lemma atoms: includes meta_term_syntax
-  shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
+lemma axiom: "dense_linear_order (op \<^loc>\<le>) (op \<^loc><)" .
+lemma atoms:
+  includes meta_term_syntax
+  shows "TERM (less :: 'a \<Rightarrow> _)"
+    and "TERM (less_eq :: 'a \<Rightarrow> _)"
+    and "TERM (op = :: 'a \<Rightarrow> _)" .
 
 declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
 declare dlo_simps[langfordsimp]
@@ -300,22 +303,22 @@
 text {* Linear order without upper bounds *}
 
 class linorder_no_ub = linorder +
-  assumes gt_ex: "\<exists>y. x \<sqsubset> y"
+  assumes gt_ex: "\<exists>y. x \<^loc>< y"
 begin
 
-lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
+lemma ge_ex: "\<exists>y. x \<^loc>\<le> y" using gt_ex by auto
 
-text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
+text {* Theorems for @{text "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
 lemma pinf_conj:
-  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-  and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
-  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
+  assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. z \<^loc><  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
 proof-
-  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
-  from gt_ex obtain z where z:"max z1 z2 \<sqsubset> z" by blast
-  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
-  {fix x assume H: "z \<sqsubset> x"
+  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+     and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast
+  from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all
+  {fix x assume H: "z \<^loc>< x"
     from less_trans[OF zz1 H] less_trans[OF zz2 H]
     have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')"  using z1 zz1 z2 zz2 by auto
   }
@@ -323,25 +326,25 @@
 qed
 
 lemma pinf_disj:
-  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-  and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
-  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
+  assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. z \<^loc><  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
 proof-
-  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
-  from gt_ex obtain z where z:"max z1 z2 \<sqsubset> z" by blast
-  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
-  {fix x assume H: "z \<sqsubset> x"
+  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+     and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast
+  from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all
+  {fix x assume H: "z \<^loc>< x"
     from less_trans[OF zz1 H] less_trans[OF zz2 H]
     have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')"  using z1 zz1 z2 zz2 by auto
   }
   thus ?thesis by blast
 qed
 
-lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
 proof-
-  from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
-  from gt_ex obtain x where x: "z \<sqsubset> x" by blast
+  from ex obtain z where z: "\<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
+  from gt_ex obtain x where x: "z \<^loc>< x" by blast
   from z x p1 show ?thesis by blast
 qed
 
@@ -350,22 +353,22 @@
 text {* Linear order without upper bounds *}
 
 class linorder_no_lb = linorder +
-  assumes lt_ex: "\<exists>y. y \<sqsubset> x"
+  assumes lt_ex: "\<exists>y. y \<^loc>< x"
 begin
 
-lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
+lemma le_ex: "\<exists>y. y \<^loc>\<le> x" using lt_ex by auto
 
 
-text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
+text {* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
 lemma minf_conj:
-  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-  and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
-  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
+  assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. x \<^loc><  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
 proof-
-  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
-  from lt_ex obtain z where z:"z \<sqsubset> min z1 z2" by blast
-  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
-  {fix x assume H: "x \<sqsubset> z"
+  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast
+  from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all
+  {fix x assume H: "x \<^loc>< z"
     from less_trans[OF H zz1] less_trans[OF H zz2]
     have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')"  using z1 zz1 z2 zz2 by auto
   }
@@ -373,24 +376,24 @@
 qed
 
 lemma minf_disj:
-  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-  and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
-  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
+  assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. x \<^loc><  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
 proof-
-  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
-  from lt_ex obtain z where z:"z \<sqsubset> min z1 z2" by blast
-  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
-  {fix x assume H: "x \<sqsubset> z"
+  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast
+  from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all
+  {fix x assume H: "x \<^loc>< z"
     from less_trans[OF H zz1] less_trans[OF H zz2]
     have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')"  using z1 zz1 z2 zz2 by auto
   }
   thus ?thesis by blast
 qed
 
-lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
 proof-
-  from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
-  from lt_ex obtain x where x: "x \<sqsubset> z" by blast
+  from ex obtain z where z: "\<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
+  from lt_ex obtain x where x: "x \<^loc>< z" by blast
   from z x p1 show ?thesis by blast
 qed
 
@@ -399,7 +402,7 @@
 
 class constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   fixes between
-  assumes between_less: "x \<sqsubset> y \<Longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y"
+  assumes between_less: "x \<^loc>< y \<Longrightarrow> x \<^loc>< between x y \<and> between x y \<^loc>< y"
      and  between_same: "between x x = x"
 
 instance advanced constr_dense_linear_order < dense_linear_order
@@ -416,41 +419,41 @@
 
 lemma rinf_U:
   assumes fU: "finite U"
-  and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
-  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
-  and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')"
+  and lin_dense: "\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P x
+  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )"
+  and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u')"
   and nmi: "\<not> MP"  and npi: "\<not> PP"  and ex: "\<exists> x.  P x"
   shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')"
 proof-
   from ex obtain x where px: "P x" by blast
-  from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto
-  then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<sqsubseteq> x" and xu':"x \<sqsubseteq> u'" by auto
+  from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u'" by auto
+  then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<^loc>\<le> x" and xu':"x \<^loc>\<le> u'" by auto
   from uU have Une: "U \<noteq> {}" by auto
   let ?l = "Min U"
   let ?u = "Max U"
   have linM: "?l \<in> U" using fU Une by simp
   have uinM: "?u \<in> U" using fU Une by simp
-  have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto
-  have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto
-  have th:"?l \<sqsubseteq> u" using uU Une lM by auto
-  from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" .
-  have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp
-  from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?u" .
+  have lM: "\<forall> t\<in> U. ?l \<^loc>\<le> t" using Une fU by auto
+  have Mu: "\<forall> t\<in> U. t \<^loc>\<le> ?u" using Une fU by auto
+  have th:"?l \<^loc>\<le> u" using uU Une lM by auto
+  from order_trans[OF th ux] have lx: "?l \<^loc>\<le> x" .
+  have th: "u' \<^loc>\<le> ?u" using uU' Une Mu by simp
+  from order_trans[OF xu' th] have xu: "x \<^loc>\<le> ?u" .
   from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu]
   have "(\<exists> s\<in> U. P s) \<or>
-      (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x)" .
+      (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U) \<and> t1 \<^loc>< x \<and> x \<^loc>< t2 \<and> P x)" .
   moreover { fix u assume um: "u\<in>U" and pu: "P u"
     have "between u u = u" by (simp add: between_same)
     with um pu have "P (between u u)" by simp
     with um have ?thesis by blast}
   moreover{
-    assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x"
+    assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U) \<and> t1 \<^loc>< x \<and> x \<^loc>< t2 \<and> P x"
       then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U"
-        and noM: "\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U" and t1x: "t1 \<sqsubset> x" and xt2: "x \<sqsubset> t2" and px: "P x"
+        and noM: "\<forall> y. t1 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U" and t1x: "t1 \<^loc>< x" and xt2: "x \<^loc>< t2" and px: "P x"
         by blast
-      from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" .
+      from less_trans[OF t1x xt2] have t1t2: "t1 \<^loc>< t2" .
       let ?u = "between t1 t2"
-      from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto
+      from between_less t1t2 have t1lu: "t1 \<^loc>< ?u" and ut2: "?u \<^loc>< t2" by auto
       from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast
       with t1M t2M have ?thesis by blast}
     ultimately show ?thesis by blast
@@ -458,11 +461,11 @@
 
 theorem fr_eq:
   assumes fU: "finite U"
-  and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
-   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
-  and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)"
-  and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)"
-  and mi: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x = MP)"  and pi: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x = PP)"
+  and lin_dense: "\<forall>x l u. (\<forall> t. l \<^loc>< t \<and> t\<^loc>< u \<longrightarrow> t \<notin> U) \<and> l\<^loc>< x \<and> x \<^loc>< u \<and> P x
+   \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )"
+  and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)"
+  and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)"
+  and mi: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x = MP)"  and pi: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x = PP)"
   shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))"
   (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D")
 proof-
@@ -472,7 +475,7 @@
    moreover {assume "MP \<or> PP" hence "?D" by blast}
    moreover {assume nmi: "\<not> MP" and npi: "\<not> PP"
      from npmibnd[OF nmibnd npibnd]
-     have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')" .
+     have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<^loc>\<le> x \<and> x \<^loc>\<le> u')" .
      from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}
    ultimately have "?D" by blast}
  moreover
@@ -492,8 +495,11 @@
 lemmas lin_dense_thms = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P
 
 lemma ferrack_axiom: "constr_dense_linear_order less_eq less between" by fact
-lemma atoms: includes meta_term_syntax
-  shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
+lemma atoms:
+  includes meta_term_syntax
+  shows "TERM (less :: 'a \<Rightarrow> _)"
+    and "TERM (less_eq :: 'a \<Rightarrow> _)"
+    and "TERM (op = :: 'a \<Rightarrow> _)" .
 
 declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms
     nmi: nmi_thms npi: npi_thms lindense:
@@ -504,7 +510,7 @@
 fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
 fun generic_whatis phi =
  let
-  val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
+  val [lt, le] = map (Morphism.term phi) [@{term "op \<^loc><"}, @{term "op \<^loc>\<le>"}]
   fun h x t =
    case term_of t of
      Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq

--- a/src/HOL/Divides.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/Divides.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -29,7 +29,7 @@
   [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
 
 class dvd_mod = times + div + zero + -- {* for code generation *}
-  assumes dvd_def_mod [code func]: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
+  assumes dvd_def_mod [code func]: "x \<^loc>dvd y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
 
 definition
   quorem :: "(nat*nat) * (nat*nat) => bool" where
@@ -880,8 +880,6 @@
 qed
 
 
-
-
 subsection {* Code generation for div, mod and dvd on nat *}
 
 definition [code func del]:

--- a/src/HOL/Finite_Set.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -2006,8 +2006,8 @@
 subsubsection{* Semi-Lattices *}
 
 locale ACIfSL = ord + ACIf +
-  assumes below_def: "x \<sqsubseteq> y \<longleftrightarrow> x \<cdot> y = x"
-  and strict_below_def: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
+  assumes below_def: "less_eq x y \<longleftrightarrow> x \<cdot> y = x"
+  and strict_below_def: "less x y \<longleftrightarrow> less_eq x y \<and> x \<noteq> y"
 begin
 
 lemma below_refl [simp]: "x \<^loc>\<le> x"
@@ -2033,9 +2033,9 @@
   then show ?thesis by (simp add: below_def)
 qed
 
-lemma below_f_conv [simp,noatp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
+lemma below_f_conv [simp,noatp]: "x \<^loc>\<le> y \<cdot> z = (x \<^loc>\<le> y \<and> x \<^loc>\<le> z)"
 proof
-  assume "x \<sqsubseteq> y \<cdot> z"
+  assume "x \<^loc>\<le> y \<cdot> z"
   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
   have "x \<cdot> y = x"
   proof -
@@ -2051,14 +2051,14 @@
     also have "\<dots> = x" by(rule xyzx)
     finally show ?thesis .
   qed
-  ultimately show "x \<sqsubseteq> y \<and> x \<sqsubseteq> z" by(simp add: below_def)
+  ultimately show "x \<^loc>\<le> y \<and> x \<^loc>\<le> z" by(simp add: below_def)
 next
-  assume a: "x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
+  assume a: "x \<^loc>\<le> y \<and> x \<^loc>\<le> z"
   hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
   have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
   also have "x \<cdot> y = x" using a by(simp_all add: below_def)
   also have "x \<cdot> z = x" using a by(simp_all add: below_def)
-  finally show "x \<sqsubseteq> y \<cdot> z" by(simp_all add: below_def)
+  finally show "x \<^loc>\<le> y \<cdot> z" by(simp_all add: below_def)
 qed
 
 end
@@ -2072,38 +2072,38 @@
 begin
 
 lemma above_f_conv:
- "x \<cdot> y \<sqsubseteq> z = (x \<sqsubseteq> z \<or> y \<sqsubseteq> z)"
+ "x \<cdot> y \<^loc>\<le> z = (x \<^loc>\<le> z \<or> y \<^loc>\<le> z)"
 proof
-  assume a: "x \<cdot> y \<sqsubseteq> z"
+  assume a: "x \<cdot> y \<^loc>\<le> z"
   have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
-  thus "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
+  thus "x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
   proof
-    assume "x \<cdot> y = x" hence "x \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
+    assume "x \<cdot> y = x" hence "x \<^loc>\<le> z" by(rule subst)(rule a) thus ?thesis ..
   next
-    assume "x \<cdot> y = y" hence "y \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
+    assume "x \<cdot> y = y" hence "y \<^loc>\<le> z" by(rule subst)(rule a) thus ?thesis ..
   qed
 next
-  assume "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
-  thus "x \<cdot> y \<sqsubseteq> z"
+  assume "x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
+  thus "x \<cdot> y \<^loc>\<le> z"
   proof
-    assume a: "x \<sqsubseteq> z"
+    assume a: "x \<^loc>\<le> z"
     have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
     also have "x \<cdot> z = x" using a by(simp add:below_def)
-    finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
+    finally show "x \<cdot> y \<^loc>\<le> z" by(simp add:below_def)
   next
-    assume a: "y \<sqsubseteq> z"
+    assume a: "y \<^loc>\<le> z"
     have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
     also have "y \<cdot> z = y" using a by(simp add:below_def)
-    finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
+    finally show "x \<cdot> y \<^loc>\<le> z" by(simp add:below_def)
   qed
 qed
 
-lemma strict_below_f_conv[simp,noatp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
+lemma strict_below_f_conv[simp,noatp]: "x \<^loc>< y \<cdot> z = (x \<^loc>< y \<and> x \<^loc>< z)"
 apply(simp add: strict_below_def)
 using lin[of y z] by (auto simp:below_def ACI)
 
 lemma strict_above_f_conv:
-  "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)"
+  "x \<cdot> y \<^loc>< z = (x \<^loc>< z \<or> y \<^loc>< z)"
 apply(simp add: strict_below_def above_f_conv)
 using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
 
@@ -2150,18 +2150,18 @@
 
 lemma (in ACIfSL) below_fold1_iff:
 assumes A: "finite A" "A \<noteq> {}"
-shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
+shows "x \<^loc>\<le> fold1 f A = (\<forall>a\<in>A. x \<^loc>\<le> a)"
 using A
 by(induct rule:finite_ne_induct) simp_all
 
 lemma (in ACIfSLlin) strict_below_fold1_iff:
-  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<sqsubset> fold1 f A = (\<forall>a\<in>A. x \<sqsubset> a)"
+  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<^loc>< fold1 f A = (\<forall>a\<in>A. x \<^loc>< a)"
 by(induct rule:finite_ne_induct) simp_all
 
 
 lemma (in ACIfSL) fold1_belowI:
 assumes A: "finite A" "A \<noteq> {}"
-shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
+shows "a \<in> A \<Longrightarrow> fold1 f A \<^loc>\<le> a"
 using A
 proof (induct rule:finite_ne_induct)
   case singleton thus ?case by simp
@@ -2173,7 +2173,7 @@
     assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
   next
     assume "a \<in> F"
-    hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
+    hence bel: "fold1 f F \<^loc>\<le> a" by(rule insert)
     have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
       using insert by(simp add:below_def ACI)
     also have "fold1 f F \<cdot> a = fold1 f F"
@@ -2186,19 +2186,19 @@
 
 lemma (in ACIfSLlin) fold1_below_iff:
 assumes A: "finite A" "A \<noteq> {}"
-shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
+shows "fold1 f A \<^loc>\<le> x = (\<exists>a\<in>A. a \<^loc>\<le> x)"
 using A
 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
 
 lemma (in ACIfSLlin) fold1_strict_below_iff:
 assumes A: "finite A" "A \<noteq> {}"
-shows "fold1 f A \<sqsubset> x = (\<exists>a\<in>A. a \<sqsubset> x)"
+shows "fold1 f A \<^loc>< x = (\<exists>a\<in>A. a \<^loc>< x)"
 using A
 by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
 
 lemma (in ACIfSLlin) fold1_antimono:
 assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
-shows "fold1 f B \<sqsubseteq> fold1 f A"
+shows "fold1 f B \<^loc>\<le> fold1 f A"
 proof(cases)
   assume "A = B" thus ?thesis by simp
 next
@@ -2213,7 +2213,7 @@
     moreover have "A Int (B-A) = {}" using prems by blast
     ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
   qed
-  also have "\<dots> \<sqsubseteq> fold1 f A" by(simp add: above_f_conv)
+  also have "\<dots> \<^loc>\<le> fold1 f A" by(simp add: above_f_conv)
   finally show ?thesis .
 qed
 
@@ -2285,7 +2285,7 @@
 where
   "Sup_fin = fold1 (op \<squnion>)"
 
-lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<sqsubseteq> \<Squnion>\<^bsub>fin\<^esub>A"
+lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<^loc>\<le> \<Squnion>\<^bsub>fin\<^esub>A"
 apply(unfold Sup_fin_def Inf_fin_def)
 apply(subgoal_tac "EX a. a:A")
 prefer 2 apply blast

--- a/src/HOL/HOL.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/HOL.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -244,8 +244,8 @@
   abs  ("\<bar>_\<bar>")
 
 class ord = type +
-  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
-    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
+  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
 
 notation

--- a/src/HOL/Library/Kleene_Algebras.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/Library/Kleene_Algebras.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -22,8 +22,8 @@
   by simp
 
 class order_by_add = idem_add + ord +
-  assumes order_def: "a \<sqsubseteq> b \<longleftrightarrow> a \<^loc>+ b = b"
-  assumes strict_order_def: "a \<sqsubset> b \<longleftrightarrow> a \<sqsubseteq> b \<and> a \<noteq> b"
+  assumes order_def: "a \<^loc>\<le> b \<longleftrightarrow> a \<^loc>+ b = b"
+  assumes strict_order_def: "a \<^loc>< b \<longleftrightarrow> a \<^loc>\<le> b \<and> a \<noteq> b"
 
 lemma ord_simp1[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> x + y = y"
   unfolding order_def .
@@ -82,14 +82,14 @@
 qed
 
 class kleene = pre_kleene + star +
-  assumes star1: "\<^loc>1 \<^loc>+ a \<^loc>* star a \<sqsubseteq> star a"
-  and star2: "\<^loc>1 \<^loc>+ star a \<^loc>* a \<sqsubseteq> star a"
-  and star3: "a \<^loc>* x \<sqsubseteq> x \<Longrightarrow> star a \<^loc>* x \<sqsubseteq> x"
-  and star4: "x \<^loc>* a \<sqsubseteq> x \<Longrightarrow> x \<^loc>* star a \<sqsubseteq> x"
+  assumes star1: "\<^loc>1 \<^loc>+ a \<^loc>* star a \<^loc>\<le> star a"
+  and star2: "\<^loc>1 \<^loc>+ star a \<^loc>* a \<^loc>\<le> star a"
+  and star3: "a \<^loc>* x \<^loc>\<le> x \<Longrightarrow> star a \<^loc>* x \<^loc>\<le> x"
+  and star4: "x \<^loc>* a \<^loc>\<le> x \<Longrightarrow> x \<^loc>* star a \<^loc>\<le> x"
 
-class kleene_by_complete_lattice =
-  pre_kleene + complete_lattice + recpower + star +
-  assumes star_cont: "a \<^loc>* star b \<^loc>* c = (SUP n. a \<^loc>* b ^ n \<^loc>* c)"
+class kleene_by_complete_lattice = pre_kleene
+  + complete_lattice + recpower + star +
+  assumes star_cont: "a \<^loc>* star b \<^loc>* c = SUPR UNIV (\<lambda>n. a \<^loc>* b \<^loc>^ n \<^loc>* c)"
 
 lemma plus_leI: 
   fixes x :: "'a :: order_by_add"

--- a/src/HOL/List.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/List.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -2542,9 +2542,9 @@
 
 class finite_intvl_succ = linorder +
 fixes successor :: "'a \<Rightarrow> 'a"
-assumes finite_intvl: "finite(ord.atLeastAtMost (op \<sqsubseteq>) a b)" (* FIXME should be finite({a..b}) *)
-and successor_incr: "a \<sqsubset> successor a"
-and ord_discrete: "\<not>(\<exists>x. a \<sqsubset> x & x \<sqsubset> successor a)"
+assumes finite_intvl: "finite(ord.atLeastAtMost (op \<^loc>\<le>) a b)" (* FIXME should be finite({a..b}) *)
+and successor_incr: "a \<^loc>< successor a"
+and ord_discrete: "\<not>(\<exists>x. a \<^loc>< x & x \<^loc>< successor a)"
 
 context finite_intvl_succ
 begin
@@ -2565,9 +2565,9 @@
 apply (metis ord_discrete less_le not_le)
 done
 
-lemma upto_rec[code]: "\<^loc>[i..j] = (if i \<sqsubseteq> j then i # \<^loc>[successor i..j] else [])"
+lemma upto_rec[code]: "\<^loc>[i..j] = (if i \<^loc>\<le> j then i # \<^loc>[successor i..j] else [])"
 proof cases
-  assume "i \<sqsubseteq> j" thus ?thesis
+  assume "i \<^loc>\<le> j" thus ?thesis
     apply(simp add:upto_def)
     apply (rule the1_equality[OF finite_sorted_distinct_unique])
      apply (simp add:finite_intvl)
@@ -2577,7 +2577,7 @@
     apply (metis successor_incr leD less_imp_le order_trans)
     done
 next
-  assume "~ i \<sqsubseteq> j" thus ?thesis
+  assume "~ i \<^loc>\<le> j" thus ?thesis
     by(simp add:upto_def atLeastAtMost_empty cong:conj_cong)
 qed
 

--- a/src/HOL/OrderedGroup.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -216,13 +216,13 @@
 subsection {* (Partially) Ordered Groups *} 
 
 class pordered_ab_semigroup_add = order + ab_semigroup_add +
-  assumes add_left_mono: "a \<sqsubseteq> b \<Longrightarrow> c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b"
+  assumes add_left_mono: "a \<^loc>\<le> b \<Longrightarrow> c \<^loc>+ a \<^loc>\<le> c \<^loc>+ b"
 
 class pordered_cancel_ab_semigroup_add =
   pordered_ab_semigroup_add + cancel_ab_semigroup_add
 
 class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
-  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b"
+  assumes add_le_imp_le_left: "c \<^loc>+ a \<^loc>\<le> c \<^loc>+ b \<Longrightarrow> a \<^loc>\<le> b"
 
 class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
 

--- a/src/HOL/Orderings.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/Orderings.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -14,13 +14,18 @@
 subsection {* Partial orders *}
 
 class order = ord +
-  assumes less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
-  and order_refl [iff]: "x \<sqsubseteq> x"
-  and order_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
-  assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
+  assumes less_le: "x \<^loc>< y \<longleftrightarrow> x \<^loc>\<le> y \<and> x \<noteq> y"
+  and order_refl [iff]: "x \<^loc>\<le> x"
+  and order_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> z"
+  assumes antisym: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
 
 begin
 
+notation (input)
+  less_eq (infix "\<sqsubseteq>" 50)
+and
+  less    (infix "\<sqsubset>" 50)
+
 text {* Reflexivity. *}
 
 lemma eq_refl: "x = y \<Longrightarrow> x \<^loc>\<le> y"

--- a/src/HOL/Real/RealVector.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -44,13 +44,19 @@
 subsection {* Real vector spaces *}
 
 class scaleR = type +
-  fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a"
-
-notation
-  scaleR (infixr "*#" 75)
+  fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<^loc>*#" 75)
+begin
 
 abbreviation
-  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a::scaleR" (infixl "'/#" 70) where
+  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "\<^loc>'/#" 70)
+where
+  "x \<^loc>/# r == scaleR (inverse r) x"
+
+end
+
+abbreviation
+  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a\<Colon>scaleR" (infixl "'/#" 70)
+where
   "x /# r == scaleR (inverse r) x"
 
 notation (xsymbols)
@@ -378,7 +384,7 @@
   real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
 
 class sgn_div_norm = scaleR + norm + sgn +
-  assumes sgn_div_norm: "sgn x = x /# norm x"
+  assumes sgn_div_norm: "sgn x = x \<^loc>/# norm x"
 
 class real_normed_vector = real_vector + sgn_div_norm +
   assumes norm_ge_zero [simp]: "0 \<le> norm x"

--- a/src/HOL/Ring_and_Field.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -153,7 +153,7 @@
 qed
 
 class field = comm_ring_1 + inverse +
-  assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
+  assumes field_inverse:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
   assumes divide_inverse: "a \<^loc>/ b = a \<^loc>* inverse b"
 
 instance field \<subseteq> division_ring
@@ -211,8 +211,8 @@
 lemmas ring_simps = group_simps ring_distribs
 
 class mult_mono = times + zero + ord +
-  assumes mult_left_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
-  assumes mult_right_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> a \<^loc>* c \<sqsubseteq> b \<^loc>* c"
+  assumes mult_left_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"
+  assumes mult_right_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> a \<^loc>* c \<^loc>\<le> b \<^loc>* c"
 
 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
 
@@ -228,8 +228,8 @@
 instance ordered_semiring \<subseteq> pordered_cancel_semiring ..
 
 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
-  assumes mult_strict_left_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
-  assumes mult_strict_right_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> a \<^loc>* c \<sqsubset> b \<^loc>* c"
+  assumes mult_strict_left_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"
+  assumes mult_strict_right_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> a \<^loc>* c \<^loc>< b \<^loc>* c"
 
 instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
 
@@ -246,7 +246,7 @@
 qed
 
 class mult_mono1 = times + zero + ord +
-  assumes mult_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
+  assumes mult_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"
 
 class pordered_comm_semiring = comm_semiring_0
   + pordered_ab_semigroup_add + mult_mono1
@@ -257,7 +257,7 @@
 instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
 
 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
-  assumes mult_strict_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
+  assumes mult_strict_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"
 
 instance pordered_comm_semiring \<subseteq> pordered_semiring
 proof
@@ -297,10 +297,10 @@
 instance lordered_ring \<subseteq> lordered_ab_group_join ..
 
 class abs_if = minus + ord + zero + abs +
-  assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
+  assumes abs_if: "abs a = (if a \<^loc>< \<^loc>0 then (uminus a) else a)"
 
 class sgn_if = sgn + zero + one + minus + ord +
-assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 \<sqsubset> x then 1 else uminus 1)"
+  assumes sgn_if: "sgn x = (if x = \<^loc>0 then \<^loc>0 else if \<^loc>0 \<^loc>< x then \<^loc>1 else uminus \<^loc>1)"
 
 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
@@ -327,7 +327,7 @@
 
 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   (*previously ordered_semiring*)
-  assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
+  assumes zero_less_one [simp]: "\<^loc>0 \<^loc>< \<^loc>1"
 
 lemma pos_add_strict:
   fixes a b c :: "'a\<Colon>ordered_semidom"

--- a/src/HOL/SetInterval.thy	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/HOL/SetInterval.thy	Sat Sep 29 08:58:51 2007 +0200
@@ -17,19 +17,19 @@
 begin
 definition
   lessThan    :: "'a => 'a set"	("(1\<^loc>{..<_})") where
-  "\<^loc>{..<u} == {x. x \<sqsubset> u}"
+  "\<^loc>{..<u} == {x. x \<^loc>< u}"
 
 definition
   atMost      :: "'a => 'a set"	("(1\<^loc>{.._})") where
-  "\<^loc>{..u} == {x. x \<sqsubseteq> u}"
+  "\<^loc>{..u} == {x. x \<^loc>\<le> u}"
 
 definition
   greaterThan :: "'a => 'a set"	("(1\<^loc>{_<..})") where
-  "\<^loc>{l<..} == {x. l\<sqsubset>x}"
+  "\<^loc>{l<..} == {x. l\<^loc><x}"
 
 definition
   atLeast     :: "'a => 'a set"	("(1\<^loc>{_..})") where
-  "\<^loc>{l..} == {x. l\<sqsubseteq>x}"
+  "\<^loc>{l..} == {x. l\<^loc>\<le>x}"
 
 definition
   greaterThanLessThan :: "'a => 'a => 'a set"  ("(1\<^loc>{_<..<_})") where

--- a/src/Pure/Isar/class.ML	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/Pure/Isar/class.ML	Sat Sep 29 08:58:51 2007 +0200
@@ -13,9 +13,9 @@
     -> ((bstring * Attrib.src list) * string list) list
     -> theory -> class * theory
   val classrel_cmd: xstring * xstring -> theory -> Proof.state
-  val class: bstring -> class list -> Element.context_i Locale.element list
+  val class: bool -> bstring -> class list -> Element.context_i Locale.element list
     -> string list -> theory -> string * Proof.context
-  val class_cmd: bstring -> xstring list -> Element.context Locale.element list
+  val class_cmd: bool -> bstring -> xstring list -> Element.context Locale.element list
     -> xstring list -> theory -> string * Proof.context
   val add_const_in_class: string -> (string * term) * Syntax.mixfix
     -> theory -> theory
@@ -25,6 +25,7 @@
   val intro_classes_tac: thm list -> tactic
   val default_intro_classes_tac: thm list -> tactic
   val class_of_locale: theory -> string -> class option
+  val local_syntax: theory -> class -> bool
   val print_classes: theory -> unit
 
   val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
@@ -46,12 +47,12 @@
   val params_of_sort: theory -> sort -> (string * (string * typ)) list
 
   (*experimental*)
-  val init_ref: (class -> Proof.context -> (theory -> theory) * Proof.context) ref
-  val init: class -> Proof.context -> (theory -> theory) * Proof.context;
-  val init_default: class -> Proof.context -> (theory -> theory) * Proof.context;
-  val remove_constraints: class -> theory -> (string * typ) list * theory
-  val class_term_check: theory -> class -> term list -> Proof.context -> term list * Proof.context
-  val local_param: theory -> class -> string -> (term * (class * int)) option
+  val init_ref: (sort -> Proof.context -> Proof.context) ref
+  val init: sort -> Proof.context -> Proof.context;
+  val init_default: sort -> Proof.context -> Proof.context;
+  val local_param: theory -> sort -> string -> (term * (class * int)) option
+  val remove_constraints': sort -> theory -> (string * typ) list * theory
+  val remove_constraints: sort -> Proof.context -> (string * typ) list * Proof.context
 end;
 
 structure Class : CLASS =
@@ -99,7 +100,7 @@
       | NONE => thm;
   in strip end;
 
-fun get_remove_contraint c thy =
+fun get_remove_constraint c thy =
   let
     val ty = Sign.the_const_constraint thy c;
   in
@@ -298,7 +299,7 @@
       #> after_qed defs;
   in
     theory
-    |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
+    |> fold_map get_remove_constraint (map fst cs |> distinct (op =))
     ||>> fold_map add_def defs
     ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
     |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
@@ -329,26 +330,27 @@
   locale: string,
   consts: (string * string) list
     (*locale parameter ~> theory constant name*),
-  v: string,
+  local_sort: sort,
   inst: typ Symtab.table * term Symtab.table
     (*canonical interpretation*),
   intro: thm,
+  local_syntax: bool,
   defs: thm list,
   localized: (string * (term * (class * int))) list
     (*theory constant name ~> (locale parameter, (class, instantiaton index of class typ))*)
 };
 
 fun rep_class_data (ClassData d) = d;
-fun mk_class_data ((locale, consts, v, inst, intro), (defs, localized)) =
-  ClassData { locale = locale, consts = consts, v = v, inst = inst, intro = intro,
-    defs = defs, localized = localized };
-fun map_class_data f (ClassData { locale, consts, v, inst, intro, defs, localized }) =
-  mk_class_data (f ((locale, consts, v, inst, intro), (defs, localized)))
-fun merge_class_data _ (ClassData { locale = locale, consts = consts, v = v, inst = inst,
-    intro = intro, defs = defs1, localized = localized1 },
-  ClassData { locale = _, consts = _, v = _, inst = _, intro = _,
+fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)) =
+  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro,
+    local_syntax = local_syntax, defs = defs, localized = localized };
+fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, localized }) =
+  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)))
+fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
+    intro = intro, local_syntax = local_syntax, defs = defs1, localized = localized1 },
+  ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _,
     defs = defs2, localized = localized2 }) =
-  mk_class_data ((locale, consts, v, inst, intro),
+  mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
     (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (localized1, localized2)));
 
 fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
@@ -393,11 +395,13 @@
   Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
     ((fst o ClassData.get) thy) [];
 
-fun these_localized thy class =
-  maps (#localized o the_class_data thy) (ancestry thy [class]);
+fun these_localized thy =
+  maps (#localized o the_class_data thy) o ancestry thy;
 
 fun local_param thy = AList.lookup (op =) o these_localized thy;
 
+fun local_syntax thy = #local_syntax o the_class_data thy
+
 fun print_classes thy =
   let
     val algebra = Sign.classes_of thy;
@@ -433,11 +437,11 @@
 
 (* updaters *)
 
-fun add_class_data ((class, superclasses), (locale, consts, v, inst, intro)) =
+fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) =
   ClassData.map (fn (gr, tab) => (
     gr
-    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, v, inst, intro),
-         ([], map (apsnd (rpair (class, 0) o Free) o swap) consts)))
+    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst,
+         intro, local_syntax), ([], map (apsnd (rpair (class, 0) o Free) o swap) consts)))
     |> fold (curry Graph.add_edge class) superclasses,
     tab
     |> Symtab.update (locale, class)
@@ -539,6 +543,90 @@
 
 (** classes and class target **)
 
+(* class context initialization *)
+
+(*experimental*)
+fun get_remove_constraint_ctxt c ctxt =
+  let
+    val ty = ProofContext.the_const_constraint ctxt c;
+  in
+    ctxt
+    |> ProofContext.add_const_constraint (c, NONE)
+    |> pair (c, ty)
+  end;
+
+fun remove_constraints' class thy =
+  thy |> fold_map (get_remove_constraint o fst) (these_localized thy class);
+
+fun remove_constraints class ctxt =
+  ctxt |> fold_map (get_remove_constraint_ctxt o fst) (these_localized (ProofContext.theory_of ctxt) class);
+
+fun default_typ ctxt constraints c =
+  case AList.lookup (op =) constraints c
+   of SOME ty => SOME ty
+    | NONE => try (Consts.the_constraint (ProofContext.consts_of ctxt)) c;
+
+fun infer_constraints ctxt constraints ts =
+    TypeInfer.infer_types (ProofContext.pp ctxt) (Sign.tsig_of (ProofContext.theory_of ctxt))
+     (Syntax.check_typs ctxt)
+      (default_typ ctxt constraints) (K NONE)
+      (Variable.names_of ctxt) true (map (rpair dummyT) ts)
+    |> #1 |> map #1
+  handle TYPE (msg, _, _) => error msg
+
+fun subst_typ local_sort =
+  map_atyps (fn (t as TFree (v, _)) => if v = AxClass.param_tyvarname
+        then TFree (v, local_sort)
+        else t
+    | t => t);
+
+fun sort_typ_check thy sort =
+  let
+    val local_sort = (#local_sort o the_class_data thy) (hd sort);
+  in
+    pair o map (subst_typ local_sort)
+  end;
+
+fun sort_term_check thy sort constraints =
+  let
+    val algebra = Sign.classes_of thy;
+    val local_sort = (#local_sort o the_class_data thy) (hd sort);
+    val v = AxClass.param_tyvarname;
+    val local_param = local_param thy sort;
+      (*FIXME efficiency*)
+    fun class_arg c idx ty =
+      let
+        val typargs = Sign.const_typargs thy (c, ty);
+        fun classtyp (TFree (w, _)) = w = v
+          | classtyp t = false;
+      in classtyp (nth typargs idx) end;
+    fun subst (t as Const (c, ty)) = (case local_param c
+         of NONE => t
+          | SOME (t', (_, idx)) => if class_arg c idx ty
+             then t' else t)
+      | subst t = t;
+  in fn ts => fn ctxt =>
+    ((map (map_aterms subst) #> infer_constraints ctxt constraints) ts, ctxt)
+  end;
+
+fun init_default sort ctxt =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val typ_check = sort_typ_check thy sort;
+    val term_check = sort_term_check thy sort;
+  in
+    ctxt
+    |> remove_constraints sort
+    ||> Variable.declare_term (Logic.mk_type (TFree (AxClass.param_tyvarname, sort)))
+    ||> Context.proof_map (Syntax.add_typ_check typ_check)
+    |-> (fn constraints =>
+        Context.proof_map (Syntax.add_term_check (term_check constraints)))
+  end;
+
+val init_ref = ref (K I : sort -> Proof.context -> Proof.context);
+fun init class = ! init_ref class;
+
+
 (* class definition *)
 
 local
@@ -551,52 +639,62 @@
     | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   end;
 
-fun gen_class add_locale prep_class prep_param bname
-    raw_supclasses raw_elems raw_other_consts thy =
+fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
   let
+    val supclasses = map (prep_class thy) raw_supclasses;
+    val sups = filter (is_some o lookup_class_data thy) supclasses
+      |> Sign.minimize_sort thy;
+    val supsort = Sign.minimize_sort thy supclasses;
+    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
+    val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
+      | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
+    val supexpr = Locale.Merge suplocales;
+    val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
+    val supconsts = AList.make (the o AList.lookup (op =) (params_of_sort thy sups))
+      (map fst supparams);
+    val mergeexpr = Locale.Merge (suplocales @ includes);
+    val constrain = Element.Constrains ((map o apsnd o map_atyps)
+      (fn TFree (_, sort) => TFree (AxClass.param_tyvarname, sort)) supparams);
+  in
+    ProofContext.init thy
+    |> Locale.cert_expr supexpr [constrain]
+    |> snd
+    |> init supsort
+    |> process_expr Locale.empty raw_elems
+    |> fst
+    |> (fn elems => ((((sups, supconsts), (supsort, mergeexpr)),
+          (*FIXME*) if null includes then constrain :: elems else elems)))
+  end;
+
+val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
+val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
+
+fun gen_class prep_spec prep_param local_syntax bname
+    raw_supclasses raw_includes_elems raw_other_consts thy =
+  let
+    val (((sups, supconsts), (supsort, mergeexpr)), elems) =
+      prep_spec thy raw_supclasses raw_includes_elems;
+    val other_consts = map (prep_param thy) raw_other_consts;
     fun mk_instT class = Symtab.empty
       |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
     fun mk_inst class param_names cs =
       Symtab.empty
       |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
            (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
-    (*FIXME need proper concept for reading locale statements*)
-    fun subst_classtyvar (_, _) =
-          TFree (AxClass.param_tyvarname, [])
-      | subst_classtyvar (v, sort) =
-          error ("Sort constraint illegal in type class, for type variable "
-            ^ v ^ "::" ^ Sign.string_of_sort thy sort);
-    (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
-      typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
-    val other_consts = map (prep_param thy) raw_other_consts;
-    val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
-      | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
-    val supclasses = map (prep_class thy) raw_supclasses;
-    val sups = filter (is_some o lookup_class_data thy) supclasses
-      |> Sign.minimize_sort thy;
-    val supsort = Sign.minimize_sort thy supclasses;
-    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
-    val supexpr = Locale.Merge (suplocales @ includes);
-    val supparams = (map fst o Locale.parameters_of_expr thy)
-      (Locale.Merge suplocales);
-    val supconsts = AList.make (the o AList.lookup (op =) (params_of_sort thy sups))
-      (map fst supparams);
-    (*val elems_constrains = map
-      (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
-    fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname,
-      if Sign.subsort thy (supsort, sort) then sort else error
-        ("Sort " ^ Sign.string_of_sort thy sort
-          ^ " is less general than permitted least general sort "
-          ^ Sign.string_of_sort thy supsort));
     fun extract_params thy name_locale =
       let
         val params = Locale.parameters_of thy name_locale;
-        val v = case (maps typ_tfrees o map (snd o fst)) params
-         of (v, _) :: _ => v
-          | [] => AxClass.param_tyvarname;
+        val local_sort = case AList.group (op =) ((maps typ_tfrees o map (snd o fst)) params)
+         of [(_, local_sort :: _)] => local_sort
+          | _ => Sign.defaultS thy
+          | vs => error ("exactly one type variable required: " ^ commas (map fst vs));
+        val _ = if Sign.subsort thy (supsort, local_sort) then () else error
+          ("Sort " ^ Sign.string_of_sort thy local_sort
+            ^ " is less general than permitted least general sort "
+            ^ Sign.string_of_sort thy supsort);
       in
-        (v, (map fst params, params
-        |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
+        (local_sort, (map fst params, params
+        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, local_sort)))
         |> (map o apsnd) (fork_mixfix true NONE #> fst)
         |> chop (length supconsts)
         |> snd))
@@ -620,19 +718,19 @@
       #> snd
   in
     thy
-    |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
+    |> Locale.add_locale_i (SOME "") bname mergeexpr elems
     |-> (fn name_locale => ProofContext.theory_result (
       `(fn thy => extract_params thy name_locale)
-      #-> (fn (v, (globals, params)) =>
+      #-> (fn (local_sort, (globals, params)) =>
         AxClass.define_class_params (bname, supsort) params
           (extract_assumes name_locale params) other_consts
       #-> (fn (name_axclass, (consts, axioms)) =>
         `(fn thy => class_intro thy name_locale name_axclass sups)
       #-> (fn class_intro =>
         add_class_data ((name_axclass, sups),
-          (name_locale, map fst params ~~ map fst consts, v,
+          (name_locale, map fst params ~~ map fst consts, local_sort,
             (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
-              (map snd supconsts @ consts)), class_intro))
+              (map snd supconsts @ consts)), class_intro, local_syntax))
       #> note_intro name_axclass class_intro
       #> class_interpretation name_axclass axioms []
       #> pair name_axclass
@@ -641,18 +739,12 @@
 
 in
 
-val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param;
-val class = gen_class Locale.add_locale_i Sign.certify_class (K I);
+val class_cmd = gen_class read_class_spec read_param;
+val class = gen_class check_class_spec (K I);
 
 end; (*local*)
 
 
-(* class target context *)
-
-fun remove_constraints class thy =
-  thy |> fold_map (get_remove_contraint o fst) (these_localized thy class);
-
-
 (* definition in class target *)
 
 fun export_fixes thy class =
@@ -673,11 +765,10 @@
         val n2 = NameSpace.qualifier n1;
         val n3 = NameSpace.base n1;
       in NameSpace.implode [n2, prfx, n3] end;
-    val v = (#v o the_class_data thy) class;
     val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
+    val rhs' = export_fixes thy class rhs;
     val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
-      if w = v then TFree (w, constrain_sort sort) else TFree var);
-    val rhs' = export_fixes thy class rhs;
+      if w = AxClass.param_tyvarname then TFree (w, constrain_sort sort) else TFree var);
     val ty' = Term.fastype_of rhs';
     val ty'' = subst_typ ty';
     val c' = mk_name c;
@@ -688,7 +779,7 @@
         val def' = symmetric def;
         val def_eq = Thm.prop_of def';
         val typargs = Sign.const_typargs thy (c', fastype_of rhs);
-        val typidx = find_index (fn TFree (w, _) => v = w | _ => false) typargs;
+        val typidx = find_index (fn TFree (w, _) => AxClass.param_tyvarname = w | _ => false) typargs;
       in
         thy
         |> class_interpretation class [def'] [def_eq]
@@ -754,52 +845,4 @@
 
 end; (*local*)
 
-(*experimental*)
-fun class_term_check thy class =
-  let
-    val algebra = Sign.classes_of thy;
-    val { v, ... } = the_class_data thy class;
-    fun add_constrain_classtyp sort' (ty as TFree (v, _)) =
-          AList.map_default (op =) (v, []) (curry (Sorts.inter_sort algebra) sort')
-      | add_constrain_classtyp sort' (Type (tyco, tys)) = case Sorts.mg_domain algebra tyco sort'
-         of sorts => fold2 add_constrain_classtyp sorts tys;
-    fun class_arg c idx ty =
-      let
-        val typargs = Sign.const_typargs thy (c, ty);
-        fun classtyp (t as TFree (w, _)) = if w = v then NONE else SOME t
-          | classtyp t = SOME t;
-      in classtyp (nth typargs idx) end;
-    fun add_inst (c, ty) (terminsts, typinsts) = case local_param thy class c
-     of NONE => (terminsts, typinsts)
-      | SOME (t, (class', idx)) => (case class_arg c idx ty
-         of NONE => (((c, ty), t) :: terminsts, typinsts)
-          | SOME ty => (terminsts, add_constrain_classtyp [class'] ty typinsts));
-  in pair o (fn ts => let
-    val cs = (fold o fold_aterms) (fn Const c_ty => insert (op =) c_ty | _ => I) ts [];
-    val (terminsts, typinsts) = fold add_inst cs ([], []);
-  in
-    ts
-    |> (map o map_aterms) (fn t as Const c_ty => the_default t (AList.lookup (op =) terminsts c_ty)
-         | t => t)
-    |> (map o map_types o map_atyps) (fn t as TFree (v, sort) =>
-         case AList.lookup (op =) typinsts v
-          of SOME sort' => TFree (v, Sorts.inter_sort algebra (sort, sort'))
-           | NONE => t)
-  end) end;
-
-val init_ref = ref (K (pair I) : class -> Proof.context -> (theory -> theory) * Proof.context);
-fun init class = ! init_ref class;
-
-fun init_default class ctxt =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val term_check = class_term_check thy class;
-  in
-    ctxt
-    (*|> ProofContext.theory_result (remove_constraints class)*)
-    |> Context.proof_map (Syntax.add_term_check term_check)
-    (*|>> fold (fn (c, ty) => Sign.add_const_constraint_i (c, SOME ty))*)
-    |> pair I
-  end;
-
 end;

--- a/src/Pure/Isar/isar_syn.ML	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Sep 29 08:58:51 2007 +0200
@@ -415,14 +415,15 @@
   OuterSyntax.command "class" "define type class" K.thy_decl (
     P.name
     -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
+    -- Scan.optional (P.$$$ "(" |-- (P.$$$ "local_syntax" >> K true) --| P.$$$ ")") false
     --| P.$$$ "=" -- (
       class_subP --| P.$$$ "+" -- class_bodyP
       || class_subP >> rpair []
       || class_bodyP >> pair [])
     -- P.opt_begin
-    >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
+    >> (fn ((((bname, add_consts), local_syntax), (supclasses, elems)), begin) =>
         Toplevel.begin_local_theory begin
-          (Class.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
+          (Class.class_cmd false bname supclasses elems add_consts #-> TheoryTarget.begin)));
 
 val instanceP =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
@@ -985,7 +986,7 @@
   "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
   "constrains", "defines", "fixes", "for", "identifier", "if",
   "imports", "in", "includes", "infix", "infixl", "infixr", "is",
-  "notes", "obtains", "open", "output", "overloaded", "shows",
+  "local_syntax", "notes", "obtains", "open", "output", "overloaded", "shows",
   "structure", "unchecked", "uses", "where", "|"];
 
 val _ = OuterSyntax.add_parsers [

--- a/src/Pure/Isar/theory_target.ML	Fri Sep 28 10:35:53 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Sat Sep 29 08:58:51 2007 +0200
@@ -359,15 +359,15 @@
     val thy = ProofContext.theory_of ctxt;
     val is_loc = loc <> "";
     val some_class = Class.class_of_locale thy loc;
-    fun class_init_exit (SOME class) =
-          Class.init class
-      | class_init_exit NONE =
-          pair I;
+    fun class_init (SOME class) =
+          Class.init [class]
+      | class_init NONE =
+          I;
   in
     ctxt
     |> Data.put (if is_loc then SOME loc else NONE)
-    |> class_init_exit some_class
-    |-> (fn exit => LocalTheory.init (NameSpace.base loc)
+    |> class_init some_class
+    |> LocalTheory.init (NameSpace.base loc)
      {pretty = pretty loc,
       consts = consts is_loc some_class,
       axioms = axioms,
@@ -382,7 +382,7 @@
       reinit = fn _ =>
         (if is_loc then Locale.init loc else ProofContext.init)
         #> begin loc,
-      exit = LocalTheory.target_of #> ProofContext.theory exit })
+      exit = LocalTheory.target_of }
   end;
 
 fun init_i NONE thy = begin "" (ProofContext.init thy)