# HG changeset patch
# User haftmann
# Date 1192569165 -7200
# Node ID af5ef0d4d6553abce361b461f23ecad6bbb99f2b
# Parent  250e1da3204b36bdd55f9a4b764514db18c175e3
global class syntax

diff -r 250e1da3204b -r af5ef0d4d655 NEWS
--- a/NEWS	Tue Oct 16 23:12:38 2007 +0200
+++ b/NEWS	Tue Oct 16 23:12:45 2007 +0200
@@ -109,6 +109,24 @@
 
 *** Pure ***
 
+* Class-context aware syntax for class target ("user space type system"):
+Local operations in class context (fixes, definitions, axiomatizations,
+abbreviations) are identified with their global counterparts during reading and
+printing of terms.  Practically, this allows to use the same syntax for
+both local *and* global operations.  Syntax declarations referring directly to
+local fixes, definitions, axiomatizations and abbreviations are applied to their
+global counterparts instead (but explicit notation declarations still are local);
+the special treatment of \<^loc> in local syntax declarations has been abandoned.
+INCOMPATIBILITY.  Most affected theories shall work after the following
+purgatory:
+
+    perl -i -pe 's/\\<\^loc>//g;' THYFILENAME1 THYFILENAME2 ...
+
+Current limitations:
+- printing of local abbreviations sometimes yields unexpected results.
+- some facilities (e.g. attribute of, legacy tac-methods) still do not use
+canonical interfaces for printing and reading terms.
+
 * Code generator: consts in 'consts_code' Isar commands are now
 referred to by usual term syntax (including optional type
 annotations).
@@ -116,7 +134,7 @@
 * Code generator: basic definitions (from 'definition', 'constdefs',
 or primitive 'instance' definitions) are added automatically to the
 table of defining equations.  Primitive defs are not used as defining
-equations by default any longer.  defining equations are now definitly
+equations by default any longer.  Defining equations are now definitly
 restricted to meta "==" and object equality "=".
 
 * The 'class' package offers a combination of axclass and locale to
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Dense_Linear_Order.thy
--- a/src/HOL/Dense_Linear_Order.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -22,153 +22,153 @@
 context linorder
 begin
 
-lemma less_not_permute: "\<not> (x \<^loc>< y \<and> y \<^loc>< x)" by (simp add: not_less linear)
+lemma less_not_permute: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
 
 lemma gather_simps: 
   shows 
-  "(\<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
+  "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y) \<and> P x)"
+  and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y) \<and> P x)"
+  "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y))"
+  and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))"  by auto
 
 lemma 
-  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)" 
+  gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)" 
   by simp
 
-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)"
+text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
+lemma minf_lt:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
+lemma minf_gt: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < 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 \<^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)"
+lemma minf_le: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma minf_ge: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
   by (auto simp add: less_le not_less not_le)
-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
+lemma minf_eq: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma minf_neq: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma minf_P: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
 
-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)"
+text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
+lemma pinf_gt:  "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
+lemma pinf_lt: "\<exists>z . \<forall>x. z < x \<longrightarrow>  (x < 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 \<^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)"
+lemma pinf_ge: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma pinf_le: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
   by (auto simp add: less_le not_less not_le)
-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 pinf_eq: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma pinf_neq: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma pinf_P: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
 
-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)"
+lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)"
   by (auto simp add: le_less)
-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  nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
+lemma  nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
+lemma  nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. u \<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 \<le> x)" by auto
+lemma  nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
+lemma  nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
+  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
+  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" by auto
+lemma  nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x) ;
+  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
+  \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<le> x)" 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  npi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x < t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by (auto simp add: le_less)
+lemma  npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
+lemma  npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<le> t \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
+lemma  npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
+lemma  npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. x \<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 \<le> u )" by auto
+lemma  npi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
+lemma  npi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ;  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
+  \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
+lemma  npi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)\<rbrakk>
+  \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<le> u)" by auto
 
-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)"
+lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y < t)"
 proof(clarsimp)
-  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"
+  fix x l u y  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x"
+    and xu: "x<u"  and px: "x < t" and ly: "l<y" and yu:"y < u"
   from tU noU ly yu have tny: "t\<noteq>y" by auto
-  {assume H: "t \<^loc>< y"
+  {assume H: "t < y"
     from less_trans[OF lx px] less_trans[OF H yu]
-    have "l \<^loc>< t \<and> t \<^loc>< u"  by simp
+    have "l < t \<and> t < u"  by simp
     with tU noU have "False" by auto}
-  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)
+  hence "\<not> t < y"  by auto hence "y \<le> t" by (simp add: not_less)
+  thus "y < t" using tny by (simp add: less_le)
 qed
 
-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)"
+lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t < y)"
 proof(clarsimp)
   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: "t \<^loc>< x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
+  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
+  and px: "t < x" and ly: "l<y" and yu:"y < u"
   from tU noU ly yu have tny: "t\<noteq>y" by auto
-  {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
+  {assume H: "y< t"
+    from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u" by simp
     with tU noU have "False" by auto}
-  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)
+  hence "\<not> y<t"  by auto hence "t \<le> y" by (auto simp add: not_less)
+  thus "t < y" using tny by (simp add:less_le)
 qed
 
-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)"
+lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)"
 proof(clarsimp)
   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>\<le> t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
+  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
+  and px: "x \<le> t" and ly: "l<y" and yu:"y < u"
   from tU noU ly yu have tny: "t\<noteq>y" by auto
-  {assume H: "t \<^loc>< y"
+  {assume H: "t < y"
     from less_le_trans[OF lx px] less_trans[OF H yu]
-    have "l \<^loc>< t \<and> t \<^loc>< u" by simp
+    have "l < t \<and> t < u" by simp
     with tU noU have "False" by auto}
-  hence "\<not> t \<^loc>< y"  by auto thus "y \<^loc>\<le> t" by (simp add: not_less)
+  hence "\<not> t < y"  by auto thus "y \<le> t" by (simp add: not_less)
 qed
 
-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)"
+lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
 proof(clarsimp)
   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: "t \<^loc>\<le> x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
+  assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
+  and px: "t \<le> x" and ly: "l<y" and yu:"y < u"
   from tU noU ly yu have tny: "t\<noteq>y" by auto
-  {assume H: "y\<^loc>< t"
+  {assume H: "y< t"
     from less_trans[OF ly H] le_less_trans[OF px xu]
-    have "l \<^loc>< t \<and> t \<^loc>< u" by simp
+    have "l < t \<and> t < u" by simp
     with tU noU have "False" by auto}
-  hence "\<not> y\<^loc><t"  by auto thus "t \<^loc>\<le> y" by (simp add: not_less)
+  hence "\<not> y<t"  by auto thus "t \<le> y" by (simp add: not_less)
 qed
-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_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x = t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)"  by auto
+lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<noteq> t   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)"  by auto
+lemma lin_dense_P: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)"  by auto
 
 lemma lin_dense_conj:
-  "\<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))"
+  "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
+  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
+  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<and> P2 x)
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
   by blast
 lemma lin_dense_disj:
-  "\<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))"
+  "\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
+  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
+  \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
+  \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<or> P2 x)
+  \<longrightarrow> (\<forall> y. l < y \<and> y < 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 \<^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')"
+lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
+  \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')"
 by auto
 
 lemma finite_set_intervals:
-  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"
+  assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
+  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
+  shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x"
 proof-
-  let ?Mx = "{y. y\<in> S \<and> y \<^loc>\<le> x}"
-  let ?xM = "{y. y\<in> S \<and> x \<^loc>\<le> y}"
+  let ?Mx = "{y. y\<in> S \<and> y \<le> x}"
+  let ?xM = "{y. y\<in> S \<and> x \<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 \<^loc>\<le> x" using Mxne fMx by auto
-  have xb:"x \<^loc>\<le> ?b" using xMne fxM by auto
+  have ax:"?a \<le> x" using Mxne fMx by auto
+  have xb:"x \<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 \<^loc>< y \<and> y \<^loc>< ?b \<longrightarrow> y \<notin> S"
+  have noy:"\<forall> y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
   proof(clarsimp)
-    fix y   assume ay: "?a \<^loc>< y" and yb: "y \<^loc>< ?b" and yS: "y \<in> S"
+    fix y   assume ay: "?a < y" and yb: "y < ?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 \<^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])}
+    moreover {assume "y \<in> ?Mx" hence "y \<le> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])}
+    moreover {assume "y \<in> ?xM" hence "?b \<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 \<^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)"
+  assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
+  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
+  shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < 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 \<^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)
+    as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S"
+    and axb: "a \<le> x \<and> x \<le> b \<and> P x"  by auto
+  from axb have "x= a \<or> x= b \<or> (a < x \<and> x < b)" by (auto simp add: le_less)
   thus ?thesis using px as bs noS by blast
 qed
 
@@ -216,45 +216,45 @@
 
 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 \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<^loc>< u)"
+  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l < 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
+  assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)"
+  then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < 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 \<^loc>< u" .}
-  thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
+    have "l < u" .}
+  thus "\<forall>l\<in>L. \<forall>u\<in>U. l < u" by blast
 next
-  assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
+  assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u"
   let ?ML = "Max L"
   let ?MU = "Min U"  
-  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
+  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<le> ?ML" by auto
+  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<le> u" by auto
+  from th1 th2 H have "?ML < ?MU" by auto
+  with dense obtain w where th3: "?ML < w" and th4: "w < ?MU" by blast
+  from th3 th1' have "\<forall>l \<in> L. l < w" by auto
+  moreover from th4 th2' have "\<forall>u \<in> U. w < u" by auto
+  ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto
 qed
 
 lemma dlo_qe_noub: 
   assumes ne: "L \<noteq> {}" and fL: "finite L"
-  shows "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> {}. x \<^loc>< y)) \<equiv> True"
+  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True"
 proof(simp add: atomize_eq)
-  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
+  from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L < M" by blast
+  from ne fL have "\<forall>x \<in> L. x \<le> Max L" by simp
+  with M have "\<forall>x\<in>L. x < M" by (auto intro: le_less_trans)
+  thus "\<exists>x. \<forall>y\<in>L. y < x" by blast
 qed
 
 lemma dlo_qe_nolb: 
   assumes ne: "U \<noteq> {}" and fU: "finite U"
-  shows "(\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> True"
+  shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
 proof(simp add: atomize_eq)
-  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
+  from lt_ex[rule_format, of "Min U"] obtain M where M: "M < Min U" by blast
+  from ne fU have "\<forall>x \<in> U. Min U \<le> x" by simp
+  with M have "\<forall>x\<in>U. M < x" by (auto intro: less_le_trans)
+  thus "\<exists>x. \<forall>y\<in>U. x < y" by blast
 qed
 
 lemma exists_neq: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x" 
@@ -263,7 +263,7 @@
 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 \<^loc>\<le>) (op \<^loc><)" .
+lemma axiom: "dense_linear_order (op \<le>) (op <)" .
 lemma atoms:
   includes meta_term_syntax
   shows "TERM (less :: 'a \<Rightarrow> _)"
@@ -303,22 +303,22 @@
 text {* Linear order without upper bounds *}
 
 class linorder_no_ub = linorder +
-  assumes gt_ex: "\<exists>y. x \<^loc>< y"
+  assumes gt_ex: "\<exists>y. x < y"
 begin
 
-lemma ge_ex: "\<exists>y. x \<^loc>\<le> y" using gt_ex by auto
+lemma ge_ex: "\<exists>y. x \<le> y" using gt_ex by auto
 
-text {* Theorems for @{text "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
+text {* Theorems for @{text "\<exists>z. \<forall>x. z < x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
 lemma pinf_conj:
-  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'))"
+  assumes ex1: "\<exists>z1. \<forall>x. z1 < x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. z2 < x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. z <  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
 proof-
-  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 ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 < x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+     and z2: "\<forall>x. z2 < x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from gt_ex obtain z where z:"max z1 z2 < z" by blast
+  from z have zz1: "z1 < z" and zz2: "z2 < z" by simp_all
+  {fix x assume H: "z < 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
   }
@@ -326,25 +326,25 @@
 qed
 
 lemma pinf_disj:
-  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'))"
+  assumes ex1: "\<exists>z1. \<forall>x. z1 < x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. z2 < x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. z <  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
 proof-
-  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 ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 < x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+     and z2: "\<forall>x. z2 < x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from gt_ex obtain z where z:"max z1 z2 < z" by blast
+  from z have zz1: "z1 < z" and zz2: "z2 < z" by simp_all
+  {fix x assume H: "z < 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 \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z < x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
 proof-
-  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 ex obtain z where z: "\<forall>x. z < x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
+  from gt_ex obtain x where x: "z < x" by blast
   from z x p1 show ?thesis by blast
 qed
 
@@ -353,22 +353,22 @@
 text {* Linear order without upper bounds *}
 
 class linorder_no_lb = linorder +
-  assumes lt_ex: "\<exists>y. y \<^loc>< x"
+  assumes lt_ex: "\<exists>y. y < x"
 begin
 
-lemma le_ex: "\<exists>y. y \<^loc>\<le> x" using lt_ex by auto
+lemma le_ex: "\<exists>y. y \<le> x" using lt_ex by auto
 
 
-text {* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
+text {* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
 lemma minf_conj:
-  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'))"
+  assumes ex1: "\<exists>z1. \<forall>x. x < z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. x < z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. x <  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
 proof-
-  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 ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x < z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x < z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from lt_ex obtain z where z:"z < min z1 z2" by blast
+  from z have zz1: "z < z1" and zz2: "z < z2" by simp_all
+  {fix x assume H: "x < 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
   }
@@ -376,24 +376,24 @@
 qed
 
 lemma minf_disj:
-  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'))"
+  assumes ex1: "\<exists>z1. \<forall>x. x < z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
+  and ex2: "\<exists>z2. \<forall>x. x < z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
+  shows "\<exists>z. \<forall>x. x <  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
 proof-
-  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 ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x < z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x < z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
+  from lt_ex obtain z where z:"z < min z1 z2" by blast
+  from z have zz1: "z < z1" and zz2: "z < z2" by simp_all
+  {fix x assume H: "x < 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 \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
 proof-
-  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 ex obtain z where z: "\<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
+  from lt_ex obtain x where x: "x < z" by blast
   from z x p1 show ?thesis by blast
 qed
 
@@ -402,7 +402,7 @@
 
 class constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   fixes between
-  assumes between_less: "x \<^loc>< y \<Longrightarrow> x \<^loc>< between x y \<and> between x y \<^loc>< y"
+  assumes between_less: "x < y \<Longrightarrow> x < between x y \<and> between x y < y"
      and  between_same: "between x x = x"
 begin
 
@@ -413,41 +413,41 @@
 
 lemma rinf_U:
   assumes fU: "finite 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 lin_dense: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P x
+  \<longrightarrow> (\<forall> y. l < y \<and> y < 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 \<le> x \<and> x \<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 \<^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 px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u'" by auto
+  then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<le> x" and xu':"x \<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 \<^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" .
+  have lM: "\<forall> t\<in> U. ?l \<le> t" using Une fU by auto
+  have Mu: "\<forall> t\<in> U. t \<le> ?u" using Une fU by auto
+  have th:"?l \<le> u" using uU Une lM by auto
+  from order_trans[OF th ux] have lx: "?l \<le> x" .
+  have th: "u' \<le> ?u" using uU' Une Mu by simp
+  from order_trans[OF xu' th] have xu: "x \<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 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U) \<and> t1 \<^loc>< x \<and> x \<^loc>< t2 \<and> P x)" .
+      (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < 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 \<^loc>< y \<and> y \<^loc>< t2 \<longrightarrow> y \<notin> U) \<and> t1 \<^loc>< x \<and> x \<^loc>< t2 \<and> P x"
+    assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U) \<and> t1 < x \<and> x < t2 \<and> P x"
       then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U"
-        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"
+        and noM: "\<forall> y. t1 < y \<and> y < t2 \<longrightarrow> y \<notin> U" and t1x: "t1 < x" and xt2: "x < t2" and px: "P x"
         by blast
-      from less_trans[OF t1x xt2] have t1t2: "t1 \<^loc>< t2" .
+      from less_trans[OF t1x xt2] have t1t2: "t1 < t2" .
       let ?u = "between t1 t2"
-      from between_less t1t2 have t1lu: "t1 \<^loc>< ?u" and ut2: "?u \<^loc>< t2" by auto
+      from between_less t1t2 have t1lu: "t1 < ?u" and ut2: "?u < 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
@@ -455,11 +455,11 @@
 
 theorem fr_eq:
   assumes fU: "finite 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 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)"
+  and lin_dense: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P x
+   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P y )"
+  and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)"
+  and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)"
+  and mi: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x = MP)"  and pi: "\<exists>z. \<forall>x. z < 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-
@@ -469,7 +469,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 \<^loc>\<le> x \<and> x \<^loc>\<le> u')" .
+     have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')" .
      from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}
    ultimately have "?D" by blast}
  moreover
@@ -504,7 +504,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 \<^loc><"}, @{term "op \<^loc>\<le>"}]
+  val [lt, le] = map (Morphism.term phi) [@{term "op <"}, @{term "op \<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
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Divides.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -12,8 +12,8 @@
 begin
 
 class div = times +
-  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>div" 70)
-  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>mod" 70)
+  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
+  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
 
 instance nat :: Divides.div
   div_def: "m div n == wfrec (pred_nat^+)
@@ -22,12 +22,12 @@
                           (%f j. if j<n | n=0 then j else f (j-n)) m" ..
 
 definition (in div)
-  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
+  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
 where
-  [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
+  [code func del]: "m dvd n \<longleftrightarrow> (\<exists>k. n = m * k)"
 
 class dvd_mod = div + zero + -- {* for code generation *}
-  assumes dvd_def_mod [code func]: "x \<^loc>dvd y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
+  assumes dvd_def_mod [code func]: "x dvd y \<longleftrightarrow> y mod x = 0"
 
 definition
   quorem :: "(nat*nat) * (nat*nat) => bool" where
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -2026,6 +2026,20 @@
   and strict_below_def: "less x y \<longleftrightarrow> less_eq x y \<and> x \<noteq> y"
 begin
 
+notation
+  less_eq  ("op \<^loc><=") and
+  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
+  less  ("op \<^loc><") and
+  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
+  
+notation (xsymbols)
+  less_eq  ("op \<^loc>\<le>") and
+  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
+
+notation (HTML output)
+  less_eq  ("op \<^loc>\<le>") and
+  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
+
 lemma below_refl [simp]: "x \<^loc>\<le> x"
   by (simp add: below_def idem)
 
@@ -2242,27 +2256,27 @@
   over (non-empty) sets by means of @{text fold1}.
 *}
 
-lemma (in lower_semilattice) ACf_inf: "ACf (op \<sqinter>)"
+lemma (in lower_semilattice) ACf_inf: "ACf inf"
   by (blast intro: ACf.intro inf_commute inf_assoc)
 
-lemma (in upper_semilattice) ACf_sup: "ACf (op \<squnion>)"
+lemma (in upper_semilattice) ACf_sup: "ACf sup"
   by (blast intro: ACf.intro sup_commute sup_assoc)
 
-lemma (in lower_semilattice) ACIf_inf: "ACIf (op \<sqinter>)"
+lemma (in lower_semilattice) ACIf_inf: "ACIf inf"
 apply(rule ACIf.intro)
 apply(rule ACf_inf)
 apply(rule ACIf_axioms.intro)
 apply(rule inf_idem)
 done
 
-lemma (in upper_semilattice) ACIf_sup: "ACIf (op \<squnion>)"
+lemma (in upper_semilattice) ACIf_sup: "ACIf sup"
 apply(rule ACIf.intro)
 apply(rule ACf_sup)
 apply(rule ACIf_axioms.intro)
 apply(rule sup_idem)
 done
 
-lemma (in lower_semilattice) ACIfSL_inf: "ACIfSL (op \<^loc>\<le>) (op \<^loc><) (op \<sqinter>)"
+lemma (in lower_semilattice) ACIfSL_inf: "ACIfSL (op \<le>) (op <) inf"
 apply(rule ACIfSL.intro)
 apply(rule ACIf.intro)
 apply(rule ACf_inf)
@@ -2275,7 +2289,7 @@
 apply(rule less_le)
 done
 
-lemma (in upper_semilattice) ACIfSL_sup: "ACIfSL (%x y. y \<^loc>\<le> x) (%x y. y \<^loc>< x) (op \<squnion>)"
+lemma (in upper_semilattice) ACIfSL_sup: "ACIfSL (%x y. y \<le> x) (%x y. y < x) sup"
 apply(rule ACIfSL.intro)
 apply(rule ACIf.intro)
 apply(rule ACf_sup)
@@ -2294,14 +2308,14 @@
 definition
   Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
 where
-  "Inf_fin = fold1 (op \<sqinter>)"
+  "Inf_fin = fold1 inf"
 
 definition
   Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
 where
-  "Sup_fin = fold1 (op \<squnion>)"
-
-lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<^loc>\<le> \<Squnion>\<^bsub>fin\<^esub>A"
+  "Sup_fin = fold1 sup"
+
+lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<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
@@ -2312,13 +2326,13 @@
 done
 
 lemma sup_Inf_absorb [simp]:
-  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>\<^bsub>fin\<^esub>A) = a"
+  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (sup a (\<Sqinter>\<^bsub>fin\<^esub>A)) = a"
 apply(subst sup_commute)
 apply(simp add: Inf_fin_def sup_absorb2 ACIfSL.fold1_belowI [OF ACIfSL_inf])
 done
 
 lemma inf_Sup_absorb [simp]:
-  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>\<^bsub>fin\<^esub>A) = a"
+  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (inf a (\<Squnion>\<^bsub>fin\<^esub>A)) = a"
 by(simp add: Sup_fin_def inf_absorb1 ACIfSL.fold1_belowI [OF ACIfSL_sup])
 
 end
@@ -2327,7 +2341,7 @@
 begin
 
 lemma sup_Inf1_distrib:
- "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<squnion> \<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{x \<squnion> a|a. a \<in> A}"
+  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
 apply(simp add: Inf_fin_def image_def
   ACIf.hom_fold1_commute[OF ACIf_inf, where h="sup x", OF sup_inf_distrib1])
 apply(rule arg_cong, blast)
@@ -2335,38 +2349,38 @@
 
 lemma sup_Inf2_distrib:
   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
-  shows "(\<Sqinter>\<^bsub>fin\<^esub>A \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
+  shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
 using A proof (induct rule: finite_ne_induct)
   case singleton thus ?case
     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
 next
   case (insert x A)
-  have finB: "finite {x \<squnion> b |b. b \<in> B}"
-    by(rule finite_surj[where f = "%b. x \<squnion> b", OF B(1)], auto)
-  have finAB: "finite {a \<squnion> b |a b. a \<in> A \<and> b \<in> B}"
+  have finB: "finite {sup x b |b. b \<in> B}"
+    by(rule finite_surj[where f = "sup x", OF B(1)], auto)
+  have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
   proof -
-    have "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<squnion> b})"
+    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
       by blast
     thus ?thesis by(simp add: insert(1) B(1))
   qed
-  have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
-  have "\<Sqinter>\<^bsub>fin\<^esub>(insert x A) \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B = (x \<sqinter> \<Sqinter>\<^bsub>fin\<^esub>A) \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B"
+  have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
+  have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
     using insert
  by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_fin_def])
-  also have "\<dots> = (x \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B) \<sqinter> (\<Sqinter>\<^bsub>fin\<^esub>A \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B)" by(rule sup_inf_distrib2)
-  also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>\<^bsub>fin\<^esub>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
+  also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
+  also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:sup_Inf1_distrib[OF B])
-  also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
+  also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})"
     (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
     using B insert
     by (simp add: Inf_fin_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
-  also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
+  also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
     by blast
   finally show ?case .
 qed
 
 lemma inf_Sup1_distrib:
- "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<sqinter> \<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{x \<sqinter> a|a. a \<in> A}"
+  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
 apply (simp add: Sup_fin_def image_def
   ACIf.hom_fold1_commute[OF ACIf_sup, where h="inf x", OF inf_sup_distrib1])
 apply (rule arg_cong, blast)
@@ -2374,31 +2388,31 @@
 
 lemma inf_Sup2_distrib:
   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
-  shows "(\<Squnion>\<^bsub>fin\<^esub>A \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
+  shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
 using A proof (induct rule: finite_ne_induct)
   case singleton thus ?case
     by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
 next
   case (insert x A)
-  have finB: "finite {x \<sqinter> b |b. b \<in> B}"
-    by(rule finite_surj[where f = "%b. x \<sqinter> b", OF B(1)], auto)
-  have finAB: "finite {a \<sqinter> b |a b. a \<in> A \<and> b \<in> B}"
+  have finB: "finite {inf x b |b. b \<in> B}"
+    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
+  have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
   proof -
-    have "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {a \<sqinter> b})"
+    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
       by blast
     thus ?thesis by(simp add: insert(1) B(1))
   qed
-  have ne: "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
-  have "\<Squnion>\<^bsub>fin\<^esub>(insert x A) \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B = (x \<squnion> \<Squnion>\<^bsub>fin\<^esub>A) \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B"
+  have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
+  have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
     using insert by (simp add: ACIf.fold1_insert_idem_def [OF ACIf_sup Sup_fin_def])
-  also have "\<dots> = (x \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B) \<squnion> (\<Squnion>\<^bsub>fin\<^esub>A \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B)" by(rule inf_sup_distrib2)
-  also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>{x \<sqinter> b|b. b \<in> B} \<squnion> \<Squnion>\<^bsub>fin\<^esub>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
+  also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
+  also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:inf_Sup1_distrib[OF B])
-  also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({x\<sqinter>b |b. b \<in> B} \<union> {a\<sqinter>b |a b. a \<in> A \<and> b \<in> B})"
+  also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})"
     (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
     using B insert
     by (simp add: Sup_fin_def ACIf.fold1_Un2[OF ACIf_sup finB _ finAB ne])
-  also have "?M = {a \<sqinter> b |a b. a \<in> insert x A \<and> b \<in> B}"
+  also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
     by blast
   finally show ?case .
 qed
@@ -2413,12 +2427,12 @@
 *}
 
 lemma Inf_fin_Inf:
-  "finite A \<Longrightarrow>  A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A = \<Sqinter>A"
+  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
 unfolding Inf_fin_def by (induct A set: finite)
    (simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf])
 
 lemma Sup_fin_Sup:
-  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>\<^bsub>fin\<^esub>A = \<Squnion>A"
+  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>\<^bsub>fin\<^esub>A = Sup A"
 unfolding Sup_fin_def by (induct A set: finite)
    (simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup])
 
@@ -2462,13 +2476,13 @@
     rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
-lemma ACIfSL_min: "ACIfSL (op \<^loc>\<le>) (op \<^loc><) min"
+lemma ACIfSL_min: "ACIfSL (op \<le>) (op <) min"
   by (rule lower_semilattice.ACIfSL_inf,
     rule lattice.axioms,
     rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
-lemma ACIfSLlin_min: "ACIfSLlin (op \<^loc>\<le>) (op \<^loc><) min"
+lemma ACIfSLlin_min: "ACIfSLlin (op \<le>) (op <) min"
   by (rule ACIfSLlin.intro,
     rule lower_semilattice.ACIfSL_inf,
     rule lattice.axioms,
@@ -2488,13 +2502,13 @@
     rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
-lemma ACIfSL_max: "ACIfSL (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
+lemma ACIfSL_max: "ACIfSL (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) max"
   by (rule upper_semilattice.ACIfSL_sup,
     rule lattice.axioms,
     rule distrib_lattice.axioms,
     rule distrib_lattice_min_max)
 
-lemma ACIfSLlin_max: "ACIfSLlin (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
+lemma ACIfSLlin_max: "ACIfSLlin (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) max"
   by (rule ACIfSLlin.intro,
     rule upper_semilattice.ACIfSL_sup,
     rule lattice.axioms,
@@ -2517,48 +2531,48 @@
   using ACf.fold1_in [OF ACf_max]
   by (fastsimp simp: Max_def max_def)
 
-lemma Min_antimono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Min N \<^loc>\<le> Min M"
+lemma Min_antimono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Min N \<le> Min M"
   by (simp add: Min_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_min])
 
-lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<^loc>\<le> Max N"
+lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<le> Max N"
   by (simp add: Max_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_max])
 
-lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x"
+lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
   by (simp add: Min_def ACIfSL.fold1_belowI [OF ACIfSL_min])
 
-lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A"
+lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
   by (simp add: Max_def ACIfSL.fold1_belowI [OF ACIfSL_max])
 
 lemma Min_ge_iff [simp,noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<^loc>\<le> a)"
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   by (simp add: Min_def ACIfSL.below_fold1_iff [OF ACIfSL_min])
 
 lemma Max_le_iff [simp,noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<^loc>\<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<^loc>\<le> x)"
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   by (simp add: Max_def ACIfSL.below_fold1_iff [OF ACIfSL_max])
 
 lemma Min_gr_iff [simp,noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>< Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<^loc>< a)"
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   by (simp add: Min_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_min])
 
 lemma Max_less_iff [simp,noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<^loc>< x \<longleftrightarrow> (\<forall>a\<in>A. a \<^loc>< x)"
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   by (simp add: Max_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_max])
 
 lemma Min_le_iff [noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<^loc>\<le> x)"
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   by (simp add: Min_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_min])
 
 lemma Max_ge_iff [noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<^loc>\<le> a)"
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   by (simp add: Max_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_max])
 
 lemma Min_less_iff [noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<^loc>< x \<longleftrightarrow> (\<exists>a\<in>A. a \<^loc>< x)"
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   by (simp add: Min_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_min])
 
 lemma Max_gr_iff [noatp]:
-  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>< Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<^loc>< a)"
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   by (simp add: Max_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_max])
 
 lemma Min_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
@@ -2586,23 +2600,29 @@
 
 lemma add_Min_commute:
   fixes k
-  shows "finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> k \<^loc>+ Min N = Min {k \<^loc>+ m | m. m \<in> N}"
-  apply (subgoal_tac "\<And>x y. k \<^loc>+ min x y = min (k \<^loc>+ x) (k \<^loc>+ y)")
-  using hom_Min_commute [of "(op \<^loc>+) k" N]
-  apply simp apply (rule arg_cong [where f = Min]) apply blast
-  apply (simp add: min_def not_le)
-  apply (blast intro: antisym less_imp_le add_left_mono)
-  done
+  assumes "finite N" and "N \<noteq> {}"
+  shows "k + Min N = Min {k + m | m. m \<in> N}"
+proof -
+  have "\<And>x y. k + min x y = min (k + x) (k + y)"
+    by (simp add: min_def not_le)
+      (blast intro: antisym less_imp_le add_left_mono)
+  with assms show ?thesis
+    using hom_Min_commute [of "plus k" N]
+    by simp (blast intro: arg_cong [where f = Min])
+qed
 
 lemma add_Max_commute:
   fixes k
-  shows "finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> k \<^loc>+ Max N = Max {k \<^loc>+ m | m. m \<in> N}"
-  apply (subgoal_tac "\<And>x y. k \<^loc>+ max x y = max (k \<^loc>+ x) (k \<^loc>+ y)")
-  using hom_Max_commute [of "(op \<^loc>+) k" N]
-  apply simp apply (rule arg_cong [where f = Max]) apply blast
-  apply (simp add: max_def not_le)
-  apply (blast intro: antisym less_imp_le add_left_mono)
-  done
+  assumes "finite N" and "N \<noteq> {}"
+  shows "k + Max N = Max {k + m | m. m \<in> N}"
+proof -
+  have "\<And>x y. k + max x y = max (k + x) (k + y)"
+    by (simp add: max_def not_le)
+      (blast intro: antisym less_imp_le add_left_mono)
+  with assms show ?thesis
+    using hom_Max_commute [of "plus k" N]
+    by simp (blast intro: arg_cong [where f = Max])
+qed
 
 end
 
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/HOL.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -208,75 +208,55 @@
   fixes default :: 'a
 
 class zero = type + 
-  fixes zero :: 'a  ("\<^loc>0")
+  fixes zero :: 'a  ("0")
 
 class one = type +
-  fixes one  :: 'a  ("\<^loc>1")
+  fixes one  :: 'a  ("1")
 
 hide (open) const zero one
 
 class plus = type +
-  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>+" 65)
+  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
 
 class minus = type +
-  fixes uminus :: "'a \<Rightarrow> 'a" 
-    and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>-" 65)
+  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
+    and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
 
 class times = type +
-  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>*" 70)
+  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
 
 class inverse = type +
   fixes inverse :: "'a \<Rightarrow> 'a"
-    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>'/" 70)
+    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
 
 class abs = type +
   fixes abs :: "'a \<Rightarrow> 'a"
 
-class sgn = type +
-  fixes sgn :: "'a \<Rightarrow> 'a"
-
-notation
-  uminus  ("- _" [81] 80)
-
 notation (xsymbols)
   abs  ("\<bar>_\<bar>")
 notation (HTML output)
   abs  ("\<bar>_\<bar>")
 
+class sgn = type +
+  fixes sgn :: "'a \<Rightarrow> 'a"
+
 class ord = type +
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 begin
 
-notation
-  less_eq  ("op \<^loc><=") and
-  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
-  less  ("op \<^loc><") and
-  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
-  
-notation (xsymbols)
-  less_eq  ("op \<^loc>\<le>") and
-  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
-
-notation (HTML output)
-  less_eq  ("op \<^loc>\<le>") and
-  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
+abbreviation (input)
+  greater_eq  (infix ">=" 50) where
+  "x >= y \<equiv> less_eq y x"
 
 abbreviation (input)
-  greater_eq  (infix "\<^loc>>=" 50) where
-  "x \<^loc>>= y \<equiv> y \<^loc><= x"
-
-notation (input)
-  greater_eq  (infix "\<^loc>\<ge>" 50)
-
-abbreviation (input)
-  greater  (infix "\<^loc>>" 50) where
-  "x \<^loc>> y \<equiv> y \<^loc>< x"
+  greater  (infix ">" 50) where
+  "x > y \<equiv> less y x"
 
 definition
-  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "\<^loc>LEAST " 10)
+  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10)
 where
-  "Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<^loc>\<le> y))"
+  "Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> less_eq x y))"
 
 end
 
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Hyperreal/HDeriv.thy
--- a/src/HOL/Hyperreal/HDeriv.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Hyperreal/HDeriv.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -369,7 +369,7 @@
 
 subsubsection {* Equivalence of NS and Standard definitions *}
 
-lemma divideR_eq_divide: "x /# y = x / y"
+lemma divideR_eq_divide: "x /\<^sub>R y = x / y"
 by (simp add: real_scaleR_def divide_inverse mult_commute)
 
 text{*Now equivalence between NSDERIV and DERIV*}
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Hyperreal/HLim.thy
--- a/src/HOL/Hyperreal/HLim.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Hyperreal/HLim.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -52,12 +52,12 @@
 by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
 
 lemma starfun_scaleR [simp]:
-  "starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
+  "starfun (\<lambda>x. f x *\<^sub>R g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
 by transfer (rule refl)
 
 lemma NSLIM_scaleR:
   "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) *# g(x)) -- x --NS> (l *# m)"
+      ==> (%x. f(x) *\<^sub>R g(x)) -- x --NS> (l *\<^sub>R m)"
 by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
 
 lemma NSLIM_add:
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -87,7 +87,7 @@
 
 lemma hnorm_scaleR:
   "\<And>x::'a::real_normed_vector star.
-   hnorm (a *# x) = \<bar>star_of a\<bar> * hnorm x"
+   hnorm (a *\<^sub>R x) = \<bar>star_of a\<bar> * hnorm x"
 by transfer (rule norm_scaleR)
 
 lemma hnorm_scaleHR:
@@ -429,7 +429,7 @@
 done
 
 lemma Infinitesimal_scaleR2:
-  "x \<in> Infinitesimal ==> a *# x \<in> Infinitesimal"
+  "x \<in> Infinitesimal ==> a *\<^sub>R x \<in> Infinitesimal"
 apply (case_tac "a = 0", simp)
 apply (rule InfinitesimalI)
 apply (drule InfinitesimalD)
@@ -853,7 +853,7 @@
 by transfer (rule scaleR_left_diff_distrib)
 
 lemma approx_scaleR1:
-  "[| a @= star_of b; c: HFinite|] ==> scaleHR a c @= b *# c"
+  "[| a @= star_of b; c: HFinite|] ==> scaleHR a c @= b *\<^sub>R c"
 apply (unfold approx_def)
 apply (drule (1) Infinitesimal_HFinite_scaleHR)
 apply (simp only: scaleHR_left_diff_distrib)
@@ -861,12 +861,12 @@
 done
 
 lemma approx_scaleR2:
-  "a @= b ==> c *# a @= c *# b"
+  "a @= b ==> c *\<^sub>R a @= c *\<^sub>R b"
 by (simp add: approx_def Infinitesimal_scaleR2
               scaleR_right_diff_distrib [symmetric])
 
 lemma approx_scaleR_HFinite:
-  "[|a @= star_of b; c @= d; d: HFinite|] ==> scaleHR a c @= b *# d"
+  "[|a @= star_of b; c @= d; d: HFinite|] ==> scaleHR a c @= b *\<^sub>R d"
 apply (rule approx_trans)
 apply (rule_tac [2] approx_scaleR2)
 apply (rule approx_scaleR1)
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -437,7 +437,7 @@
 
 definition
   exp :: "'a \<Rightarrow> 'a::{recpower,real_normed_field,banach}" where
-  "exp x = (\<Sum>n. x ^ n /# real (fact n))"
+  "exp x = (\<Sum>n. x ^ n /\<^sub>R real (fact n))"
 
 definition
   sin :: "real => real" where
@@ -451,10 +451,10 @@
 
 lemma summable_exp_generic:
   fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
-  defines S_def: "S \<equiv> \<lambda>n. x ^ n /# real (fact n)"
+  defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
   shows "summable S"
 proof -
-  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /# real (Suc n)"
+  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
     unfolding S_def by (simp add: power_Suc del: mult_Suc)
   obtain r :: real where r0: "0 < r" and r1: "r < 1"
     using dense [OF zero_less_one] by fast
@@ -481,12 +481,12 @@
 
 lemma summable_norm_exp:
   fixes x :: "'a::{real_normed_algebra_1,recpower,banach}"
-  shows "summable (\<lambda>n. norm (x ^ n /# real (fact n)))"
+  shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
 proof (rule summable_norm_comparison_test [OF exI, rule_format])
-  show "summable (\<lambda>n. norm x ^ n /# real (fact n))"
+  show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
     by (rule summable_exp_generic)
 next
-  fix n show "norm (x ^ n /# real (fact n)) \<le> norm x ^ n /# real (fact n)"
+  fix n show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
     by (simp add: norm_scaleR norm_power_ineq)
 qed
 
@@ -536,7 +536,7 @@
 apply (case_tac [2] "n", auto)
 done
 
-lemma exp_converges: "(\<lambda>n. x ^ n /# real (fact n)) sums exp x"
+lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
 unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
 
 lemma sin_converges: 
@@ -604,7 +604,7 @@
                   else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
 by (auto intro!: sums_unique sums_minus sin_converges)
 
-lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /# real (fact n))"
+lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
 by (auto intro!: ext simp add: exp_def)
 
 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
@@ -680,7 +680,7 @@
 
 lemma exp_series_add:
   fixes x y :: "'a::{real_field,recpower}"
-  defines S_def: "S \<equiv> \<lambda>x n. x ^ n /# real (fact n)"
+  defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
   shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
 proof (induct n)
   case 0
@@ -688,12 +688,12 @@
     unfolding S_def by simp
 next
   case (Suc n)
-  have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /# real (Suc n)"
+  have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
     unfolding S_def by (simp add: power_Suc del: mult_Suc)
-  hence times_S: "\<And>x n. x * S x n = real (Suc n) *# S x (Suc n)"
+  hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
     by simp
 
-  have "real (Suc n) *# S (x + y) (Suc n) = (x + y) * S (x + y) n"
+  have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
     by (simp only: times_S)
   also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (n-i))"
     by (simp only: Suc)
@@ -703,21 +703,21 @@
   also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
                 + (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
     by (simp only: setsum_right_distrib mult_ac)
-  also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *# (S x (Suc i) * S y (n-i)))
-                + (\<Sum>i=0..n. real (Suc n-i) *# (S x i * S y (Suc n-i)))"
+  also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
+                + (\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
     by (simp add: times_S Suc_diff_le)
-  also have "(\<Sum>i=0..n. real (Suc i) *# (S x (Suc i) * S y (n-i))) =
-             (\<Sum>i=0..Suc n. real i *# (S x i * S y (Suc n-i)))"
+  also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
+             (\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
     by (subst setsum_cl_ivl_Suc2, simp)
-  also have "(\<Sum>i=0..n. real (Suc n-i) *# (S x i * S y (Suc n-i))) =
-             (\<Sum>i=0..Suc n. real (Suc n-i) *# (S x i * S y (Suc n-i)))"
+  also have "(\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
+             (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
     by (subst setsum_cl_ivl_Suc, simp)
-  also have "(\<Sum>i=0..Suc n. real i *# (S x i * S y (Suc n-i))) +
-             (\<Sum>i=0..Suc n. real (Suc n-i) *# (S x i * S y (Suc n-i))) =
-             (\<Sum>i=0..Suc n. real (Suc n) *# (S x i * S y (Suc n-i)))"
+  also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
+             (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
+             (\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
     by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
               real_of_nat_add [symmetric], simp)
-  also have "\<dots> = real (Suc n) *# (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
+  also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
     by (simp only: scaleR_right.setsum)
   finally show
     "S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Lattices.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -33,18 +33,20 @@
 lemmas antisym_intro [intro!] = antisym
 lemmas (in -) [rule del] = antisym_intro
 
-lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
-apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
- apply(blast intro: order_trans)
-apply simp
-done
+lemma le_infI1[intro]:
+  assumes "a \<sqsubseteq> x"
+  shows "a \<sqinter> b \<sqsubseteq> x"
+proof (rule order_trans)
+  show "a \<sqinter> b \<sqsubseteq> a" and "a \<sqsubseteq> x" using assms by simp
+qed
 lemmas (in -) [rule del] = le_infI1
 
-lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
-apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
- apply(blast intro: order_trans)
-apply simp
-done
+lemma le_infI2[intro]:
+  assumes "b \<sqsubseteq> x"
+  shows "a \<sqinter> b \<sqsubseteq> x"
+proof (rule order_trans)
+  show "a \<sqinter> b \<sqsubseteq> b" and "b \<sqsubseteq> x" using assms by simp
+qed
 lemmas (in -) [rule del] = le_infI2
 
 lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
@@ -75,17 +77,11 @@
 lemmas (in -) [rule del] = antisym_intro
 
 lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
-apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
- apply(blast intro: order_trans)
-apply simp
-done
+  by (rule order_trans) auto
 lemmas (in -) [rule del] = le_supI1
 
 lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
-apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
- apply(blast intro: order_trans)
-apply simp
-done
+  by (rule order_trans) auto 
 lemmas (in -) [rule del] = le_supI2
 
 lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
@@ -255,26 +251,26 @@
 
 lemma (in lower_semilattice) inf_unique:
   fixes f (infixl "\<triangle>" 70)
-  assumes le1: "\<And>x y. x \<triangle> y \<^loc>\<le> x" and le2: "\<And>x y. x \<triangle> y \<^loc>\<le> y"
-  and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z"
+  assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
+  and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
   shows "x \<sqinter> y = x \<triangle> y"
 proof (rule antisym)
-  show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
+  show "x \<triangle> y \<le> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
 next
-  have leI: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" by (blast intro: greatest)
-  show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all
+  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
+  show "x \<sqinter> y \<le> x \<triangle> y" by (rule leI) simp_all
 qed
 
 lemma (in upper_semilattice) sup_unique:
   fixes f (infixl "\<nabla>" 70)
-  assumes ge1 [simp]: "\<And>x y. x \<^loc>\<le> x \<nabla> y" and ge2: "\<And>x y. y \<^loc>\<le> x \<nabla> y"
-  and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x"
+  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
+  and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
   shows "x \<squnion> y = x \<nabla> y"
 proof (rule antisym)
-  show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
+  show "x \<squnion> y \<le> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
 next
-  have leI: "\<And>x y z. x \<^loc>\<le> z \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<nabla> y \<^loc>\<le> z" by (blast intro: least)
-  show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all
+  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
+  show "x \<nabla> y \<le> x \<squnion> y" by (rule leI) simp_all
 qed
   
 
@@ -282,9 +278,9 @@
   special case of @{const inf}/@{const sup} *}
 
 lemma (in linorder) distrib_lattice_min_max:
-  "distrib_lattice (op \<^loc>\<le>) (op \<^loc><) min max"
+  "distrib_lattice (op \<le>) (op <) min max"
 proof unfold_locales
-  have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
+  have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
     by (auto simp add: less_le antisym)
   fix x y z
   show "max x (min y z) = min (max x y) (max x z)"
@@ -333,10 +329,10 @@
      and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
 begin
 
-lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}"
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
   by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
 
-lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
+lemma Sup_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
   by (auto intro: Inf_lower Inf_greatest Sup_upper Sup_least)
 
 lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
@@ -411,10 +407,10 @@
 where
   "bot = Sup {}"
 
-lemma top_greatest [simp]: "x \<^loc>\<le> top"
+lemma top_greatest [simp]: "x \<le> top"
   by (unfold top_def, rule Inf_greatest, simp)
 
-lemma bot_least [simp]: "bot \<^loc>\<le> x"
+lemma bot_least [simp]: "bot \<le> x"
   by (unfold bot_def, rule Sup_least, simp)
 
 definition
@@ -584,4 +580,16 @@
 lemmas inf_aci = inf_ACI
 lemmas sup_aci = sup_ACI
 
+no_notation
+  inf (infixl "\<sqinter>" 70)
+
+no_notation
+  sup (infixl "\<squnion>" 65)
+
+no_notation
+  Inf ("\<Sqinter>_" [900] 900)
+
+no_notation
+  Sup ("\<Squnion>_" [900] 900)
+
 end
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Library/Kleene_Algebras.thy
--- a/src/HOL/Library/Kleene_Algebras.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Library/Kleene_Algebras.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -15,15 +15,15 @@
   fixes star :: "'a \<Rightarrow> 'a"
 
 class idem_add = ab_semigroup_add +
-  assumes add_idem [simp]: "x \<^loc>+ x = x"
+  assumes add_idem [simp]: "x + x = x"
 
 lemma add_idem2[simp]: "(x::'a::idem_add) + (x + y) = x + y"
   unfolding add_assoc[symmetric]
   by simp
 
 class order_by_add = idem_add + ord +
-  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"
+  assumes order_def: "a \<le> b \<longleftrightarrow> a + b = b"
+  assumes strict_order_def: "a < b \<longleftrightarrow> a \<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 \<^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"
+  assumes star1: "1 + a * star a \<le> star a"
+  and star2: "1 + star a * a \<le> star a"
+  and star3: "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
+  and star4: "x * a \<le> x \<Longrightarrow> x * star a \<le> x"
 
 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)"
+  assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
 
 lemma plus_leI: 
   fixes x :: "'a :: order_by_add"
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Library/Quicksort.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -14,7 +14,7 @@
 
 function quicksort :: "'a list \<Rightarrow> 'a list" where
 "quicksort []     = []" |
-"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<^loc>\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<^loc>\<le>y])"
+"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
 by pat_completeness auto
 
 termination
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Library/Quotient.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -22,12 +22,12 @@
 *}
 
 class eqv = type +
-  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<^loc>\<sim>" 50)
+  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
 
 class equiv = eqv +
-  assumes equiv_refl [intro]: "x \<^loc>\<sim> x"
-  assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z"
-  assumes equiv_sym [sym]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> x"
+  assumes equiv_refl [intro]: "x \<sim> x"
+  assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
+  assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
 
 lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
 proof -
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/List.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -218,11 +218,11 @@
 fun (in linorder) sorted :: "'a list \<Rightarrow> bool" where
 "sorted [] \<longleftrightarrow> True" |
 "sorted [x] \<longleftrightarrow> True" |
-"sorted (x#y#zs) \<longleftrightarrow> x \<^loc><= y \<and> sorted (y#zs)"
+"sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
 
 fun (in linorder) insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "insort x [] = [x]" |
-"insort x (y#ys) = (if x \<^loc><= y then (x#y#ys) else y#(insort x ys))"
+"insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
 
 fun (in linorder) sort :: "'a list \<Rightarrow> 'a list" where
 "sort [] = []" |
@@ -1816,11 +1816,11 @@
 by (induct k arbitrary: a b l) simp_all
 
 lemma (in semigroup_add) foldl_assoc:
-shows "foldl op\<^loc>+ (x\<^loc>+y) zs = x \<^loc>+ (foldl op\<^loc>+ y zs)"
+shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
 by (induct zs arbitrary: y) (simp_all add:add_assoc)
 
 lemma (in monoid_add) foldl_absorb0:
-shows "x \<^loc>+ (foldl op\<^loc>+ \<^loc>0 zs) = foldl op\<^loc>+ x zs"
+shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
 by (induct zs) (simp_all add:foldl_assoc)
 
 
@@ -1843,7 +1843,7 @@
 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
 
-lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op \<^loc>+ xs a = foldl op \<^loc>+ a xs"
+lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
   by (induct xs, auto simp add: foldl_assoc add_commute)
 
 text {*
@@ -2526,12 +2526,12 @@
 context linorder
 begin
 
-lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x \<^loc><= y))"
+lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
 apply(induct xs arbitrary: x) apply simp
 by simp (blast intro: order_trans)
 
 lemma sorted_append:
-  "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<^loc>\<le>y))"
+  "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
 by (induct xs) (auto simp add:sorted_Cons)
 
 lemma set_insort: "set(insort x xs) = insert x (set xs)"
@@ -2583,32 +2583,32 @@
 
 class finite_intvl_succ = linorder +
 fixes successor :: "'a \<Rightarrow> '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)"
+assumes finite_intvl: "finite(ord.atLeastAtMost (op \<le>) a b)" (* FIXME should be finite({a..b}) *)
+and successor_incr: "a < successor a"
+and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
 
 context finite_intvl_succ
 begin
 
 definition
- upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1\<^loc>[_../_])") where
-"upto i j == THE is. set is = \<^loc>{i..j} & sorted is & distinct is"
-
-lemma set_upto[simp]: "set\<^loc>[a..b] = \<^loc>{a..b}"
+ upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
+"upto i j == THE is. set is = {i..j} & sorted is & distinct is"
+
+lemma set_upto[simp]: "set[a..b] = {a..b}"
 apply(simp add:upto_def)
 apply(rule the1I2)
 apply(simp_all add: finite_sorted_distinct_unique finite_intvl)
 done
 
-lemma insert_intvl: "i \<^loc>\<le> j \<Longrightarrow> insert i \<^loc>{successor i..j} = \<^loc>{i..j}"
+lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
 apply(insert successor_incr[of i])
 apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
 apply (metis ord_discrete less_le not_le)
 done
 
-lemma upto_rec[code]: "\<^loc>[i..j] = (if i \<^loc>\<le> j then i # \<^loc>[successor i..j] else [])"
+lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
 proof cases
-  assume "i \<^loc>\<le> j" thus ?thesis
+  assume "i \<le> j" thus ?thesis
     apply(simp add:upto_def)
     apply (rule the1_equality[OF finite_sorted_distinct_unique])
      apply (simp add:finite_intvl)
@@ -2618,7 +2618,7 @@
     apply (metis successor_incr leD less_imp_le order_trans)
     done
 next
-  assume "~ i \<^loc>\<le> j" thus ?thesis
+  assume "~ i \<le> j" thus ?thesis
     by(simp add:upto_def atLeastAtMost_empty cong:conj_cong)
 qed
 
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Nat.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -1154,7 +1154,7 @@
 begin
 
 definition
-  of_nat_def: "of_nat = nat_rec \<^loc>0 (\<lambda>_. (op \<^loc>+) \<^loc>1)"
+  of_nat_def: "of_nat = nat_rec 0 (\<lambda>_. (op +) 1)"
 
 end
 
@@ -1340,8 +1340,8 @@
 begin
 
 lemma of_nat_simps [simp, code]:
-  shows of_nat_0:   "of_nat 0 = \<^loc>0"
-    and of_nat_Suc: "of_nat (Suc m) = \<^loc>1 \<^loc>+ of_nat m"
+  shows of_nat_0:   "of_nat 0 = 0"
+    and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
   unfolding of_nat_def by simp_all
 
 end
@@ -1405,7 +1405,7 @@
 
 class semiring_char_0 = semiring_1 +
   assumes of_nat_eq_iff [simp]:
-    "(Nat.semiring_1.of_nat \<^loc>1 \<^loc>0 (op \<^loc>+) m = Nat.semiring_1.of_nat \<^loc>1 \<^loc>0 (op \<^loc>+)  n) = (m = n)"
+    "of_nat m = of_nat n \<longleftrightarrow> m = n"
 
 text{*Every @{text ordered_semidom} has characteristic zero.*}
 instance ordered_semidom < semiring_char_0
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -27,58 +27,75 @@
 subsection {* Semigroups and Monoids *}
 
 class semigroup_add = plus +
-  assumes add_assoc: "(a \<^loc>+ b) \<^loc>+ c = a \<^loc>+ (b \<^loc>+ c)"
+  assumes add_assoc: "(a + b) + c = a + (b + c)"
 
 class ab_semigroup_add = semigroup_add +
-  assumes add_commute: "a \<^loc>+ b = b \<^loc>+ a"
+  assumes add_commute: "a + b = b + a"
+begin
 
-lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ab_semigroup_add))"
-  by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
+lemma add_left_commute: "a + (b + c) = b + (a + c)"
+  by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
+  (*FIXME term_check*)
+
+theorems add_ac = add_assoc add_commute add_left_commute
+
+end
 
 theorems add_ac = add_assoc add_commute add_left_commute
 
 class semigroup_mult = times +
-  assumes mult_assoc: "(a \<^loc>* b) \<^loc>* c = a \<^loc>* (b \<^loc>* c)"
+  assumes mult_assoc: "(a * b) * c = a * (b * c)"
 
 class ab_semigroup_mult = semigroup_mult +
-  assumes mult_commute: "a \<^loc>* b = b \<^loc>* a"
+  assumes mult_commute: "a * b = b * a"
 begin
 
-lemma mult_left_commute: "a \<^loc>* (b \<^loc>* c) = b \<^loc>* (a \<^loc>* c)"
-  by (rule mk_left_commute [of "op \<^loc>*", OF mult_assoc mult_commute])
+lemma mult_left_commute: "a * (b * c) = b * (a * c)"
+  by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
+  (*FIXME term_check*)
+
+theorems mult_ac = mult_assoc mult_commute mult_left_commute
 
 end
 
 theorems mult_ac = mult_assoc mult_commute mult_left_commute
 
 class monoid_add = zero + semigroup_add +
-  assumes add_0_left [simp]: "\<^loc>0 \<^loc>+ a = a" and add_0_right [simp]: "a \<^loc>+ \<^loc>0 = a"
+  assumes add_0_left [simp]: "0 + a = a"
+    and add_0_right [simp]: "a + 0 = a"
 
 class comm_monoid_add = zero + ab_semigroup_add +
-  assumes add_0: "\<^loc>0 \<^loc>+ a = a"
+  assumes add_0: "0 + a = a"
+begin
 
-instance comm_monoid_add < monoid_add
-by intro_classes (insert comm_monoid_add_class.zero_plus.add_0, simp_all add: add_commute, auto)
+subclass monoid_add
+  by unfold_locales (insert add_0, simp_all add: add_commute)
+
+end
 
 class monoid_mult = one + semigroup_mult +
-  assumes mult_1_left [simp]: "\<^loc>1 \<^loc>* a  = a"
-  assumes mult_1_right [simp]: "a \<^loc>* \<^loc>1 = a"
+  assumes mult_1_left [simp]: "1 * a  = a"
+  assumes mult_1_right [simp]: "a * 1 = a"
 
 class comm_monoid_mult = one + ab_semigroup_mult +
-  assumes mult_1: "\<^loc>1 \<^loc>* a = a"
+  assumes mult_1: "1 * a = a"
+begin
 
-instance comm_monoid_mult \<subseteq> monoid_mult
-  by intro_classes (insert mult_1, simp_all add: mult_commute, auto)
+subclass monoid_mult
+  by unfold_locales (insert mult_1, simp_all add: mult_commute) 
+
+end
 
 class cancel_semigroup_add = semigroup_add +
-  assumes add_left_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
-  assumes add_right_imp_eq: "b \<^loc>+ a = c \<^loc>+ a \<Longrightarrow> b = c"
+  assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
+  assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
 
 class cancel_ab_semigroup_add = ab_semigroup_add +
-  assumes add_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
+  assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
+begin
 
-instance cancel_ab_semigroup_add \<subseteq> cancel_semigroup_add
-proof intro_classes
+subclass cancel_semigroup_add
+proof unfold_locales
   fix a b c :: 'a
   assume "a + b = a + c" 
   then show "b = c" by (rule add_imp_eq)
@@ -89,60 +106,50 @@
   then show "b = c" by (rule add_imp_eq)
 qed
 
+end context cancel_ab_semigroup_add begin
+
 lemma add_left_cancel [simp]:
-  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
+  "a + b = a + c \<longleftrightarrow> b = c"
   by (blast dest: add_left_imp_eq)
 
 lemma add_right_cancel [simp]:
-  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
+  "b + a = c + a \<longleftrightarrow> b = c"
   by (blast dest: add_right_imp_eq)
 
+end
+
 subsection {* Groups *}
 
-class ab_group_add = minus + comm_monoid_add +
-  assumes ab_left_minus: "uminus a \<^loc>+ a = \<^loc>0"
-  assumes ab_diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
-
 class group_add = minus + monoid_add +
-  assumes left_minus [simp]: "uminus a \<^loc>+ a = \<^loc>0"
-  assumes diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
-
-instance ab_group_add < group_add
-by intro_classes (simp_all add: ab_left_minus ab_diff_minus)
+  assumes left_minus [simp]: "- a + a = 0"
+  assumes diff_minus: "a - b = a + (- b)"
+begin
 
-instance ab_group_add \<subseteq> cancel_ab_semigroup_add
-proof intro_classes
-  fix a b c :: 'a
-  assume "a + b = a + c"
-  then have "uminus a + a + b = uminus a + a + c" unfolding add_assoc by simp
-  then show "b = c" by simp
-qed
+lemma minus_add_cancel: "- a + (a + b) = b"
+  by (simp add: add_assoc[symmetric])
 
-lemma minus_add_cancel: "-(a::'a::group_add) + (a+b) = b"
-by(simp add:add_assoc[symmetric])
-
-lemma minus_zero[simp]: "-(0::'a::group_add) = 0"
+lemma minus_zero [simp]: "- 0 = 0"
 proof -
-  have "-(0::'a::group_add) = - 0 + (0+0)" by(simp only: add_0_right)
-  also have "\<dots> = 0" by(rule minus_add_cancel)
+  have "- 0 = - 0 + (0 + 0)" by (simp only: add_0_right)
+  also have "\<dots> = 0" by (rule minus_add_cancel)
   finally show ?thesis .
 qed
 
-lemma minus_minus[simp]: "- (-(a::'a::group_add)) = a"
+lemma minus_minus [simp]: "- (- a) = a"
 proof -
-  have "-(-a) = -(-a) + (-a + a)" by simp
-  also have "\<dots> = a" by(rule minus_add_cancel)
+  have "- (- a) = - (- a) + (- a + a)" by simp
+  also have "\<dots> = a" by (rule minus_add_cancel)
   finally show ?thesis .
 qed
 
-lemma right_minus[simp]: "a + - a = (0::'a::group_add)"
+lemma right_minus [simp]: "a + - a = 0"
 proof -
-  have "a + -a = -(-a) + -a" by simp
-  also have "\<dots> = 0" thm group_add.left_minus by(rule left_minus)
+  have "a + - a = - (- a) + - a" by simp
+  also have "\<dots> = 0" by (rule left_minus)
   finally show ?thesis .
 qed
 
-lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::group_add))"
+lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
 proof
   assume "a - b = 0"
   have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
@@ -152,154 +159,173 @@
   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
 qed
 
-lemma equals_zero_I: assumes "a+b = 0" shows "-a = (b::'a::group_add)"
+lemma equals_zero_I:
+  assumes "a + b = 0"
+  shows "- a = b"
 proof -
-  have "- a = -a + (a+b)" using assms by simp
-  also have "\<dots> = b" by(simp add:add_assoc[symmetric])
+  have "- a = - a + (a + b)" using assms by simp
+  also have "\<dots> = b" by (simp add: add_assoc[symmetric])
   finally show ?thesis .
 qed
 
-lemma diff_self[simp]: "(a::'a::group_add) - a = 0"
-by(simp add: diff_minus)
+lemma diff_self [simp]: "a - a = 0"
+  by (simp add: diff_minus)
 
-lemma diff_0 [simp]: "(0::'a::group_add) - a = -a"
-by (simp add: diff_minus)
+lemma diff_0 [simp]: "0 - a = - a"
+  by (simp add: diff_minus)
 
-lemma diff_0_right [simp]: "a - (0::'a::group_add) = a" 
-by (simp add: diff_minus)
+lemma diff_0_right [simp]: "a - 0 = a" 
+  by (simp add: diff_minus)
 
-lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::group_add)"
-by (simp add: diff_minus)
+lemma diff_minus_eq_add [simp]: "a - - b = a + b"
+  by (simp add: diff_minus)
 
-lemma uminus_add_conv_diff: "-a + b = b - (a::'a::ab_group_add)"
-by(simp add:diff_minus add_commute)
-
-lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::group_add))" 
+lemma neg_equal_iff_equal [simp]:
+  "- a = - b \<longleftrightarrow> a = b" 
 proof 
   assume "- a = - b"
   hence "- (- a) = - (- b)"
     by simp
-  thus "a=b" by simp
+  thus "a = b" by simp
 next
-  assume "a=b"
-  thus "-a = -b" by simp
+  assume "a = b"
+  thus "- a = - b" by simp
 qed
 
-lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::group_add))"
-by (subst neg_equal_iff_equal [symmetric], simp)
+lemma neg_equal_0_iff_equal [simp]:
+  "- a = 0 \<longleftrightarrow> a = 0"
+  by (subst neg_equal_iff_equal [symmetric], simp)
 
-lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::group_add))"
-by (subst neg_equal_iff_equal [symmetric], simp)
+lemma neg_0_equal_iff_equal [simp]:
+  "0 = - a \<longleftrightarrow> 0 = a"
+  by (subst neg_equal_iff_equal [symmetric], simp)
 
 text{*The next two equations can make the simplifier loop!*}
 
-lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::group_add))"
+lemma equation_minus_iff:
+  "a = - b \<longleftrightarrow> b = - a"
 proof -
-  have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
+  have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
+  thus ?thesis by (simp add: eq_commute)
+qed
+
+lemma minus_equation_iff:
+  "- a = b \<longleftrightarrow> - b = a"
+proof -
+  have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
   thus ?thesis by (simp add: eq_commute)
 qed
 
-lemma minus_equation_iff: "(- a = b) = (- (b::'a::group_add) = a)"
-proof -
-  have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
-  thus ?thesis by (simp add: eq_commute)
+end
+
+class ab_group_add = minus + comm_monoid_add +
+  assumes ab_left_minus: "- a + a = 0"
+  assumes ab_diff_minus: "a - b = a + (- b)"
+
+subclass (in ab_group_add) group_add
+  by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
+
+subclass (in ab_group_add) cancel_semigroup_add
+proof unfold_locales
+  fix a b c :: 'a
+  assume "a + b = a + c"
+  then have "- a + a + b = - a + a + c"
+    unfolding add_assoc by simp
+  then show "b = c" by simp
+next
+  fix a b c :: 'a
+  assume "b + a = c + a"
+  then have "b + (a + - a) = c + (a + - a)"
+    unfolding add_assoc [symmetric] by simp
+  then show "b = c" by simp
 qed
 
-lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ab_group_add)"
-apply (rule equals_zero_I)
-apply (simp add: add_ac)
-done
+subclass (in ab_group_add) cancel_ab_semigroup_add
+proof unfold_locales
+  fix a b c :: 'a
+  assume "a + b = a + c"
+  then have "- a + a + b = - a + a + c"
+    unfolding add_assoc by simp
+  then show "b = c" by simp
+qed
+
+context ab_group_add
+begin
 
-lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ab_group_add)"
-by (simp add: diff_minus add_commute)
+lemma uminus_add_conv_diff:
+  "- a + b = b - a"
+  by (simp add:diff_minus add_commute)
+
+lemma minus_add_distrib [simp]:
+  "- (a + b) = - a + - b"
+  by (rule equals_zero_I) (simp add: add_ac)
+
+lemma minus_diff_eq [simp]:
+  "- (a - b) = b - a"
+  by (simp add: diff_minus add_commute)
+
+end
 
 subsection {* (Partially) Ordered Groups *} 
 
 class pordered_ab_semigroup_add = order + ab_semigroup_add +
-  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 \<^loc>\<le> c \<^loc>+ b \<Longrightarrow> a \<^loc>\<le> b"
-
-class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
-
-instance pordered_ab_group_add \<subseteq> pordered_ab_semigroup_add_imp_le
-proof
-  fix a b c :: 'a
-  assume "c + a \<le> c + b"
-  hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
-  hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
-  thus "a \<le> b" by simp
-qed
-
-class ordered_ab_semigroup_add =
-  linorder + pordered_ab_semigroup_add
+  assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
+begin
 
-class ordered_cancel_ab_semigroup_add =
-  linorder + pordered_cancel_ab_semigroup_add
-
-instance ordered_cancel_ab_semigroup_add \<subseteq> ordered_ab_semigroup_add ..
-
-instance ordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add_imp_le
-proof
-  fix a b c :: 'a
-  assume le: "c + a <= c + b"  
-  show "a <= b"
-  proof (rule ccontr)
-    assume w: "~ a \<le> b"
-    hence "b <= a" by (simp add: linorder_not_le)
-    hence le2: "c+b <= c+a" by (rule add_left_mono)
-    have "a = b" 
-      apply (insert le)
-      apply (insert le2)
-      apply (drule order_antisym, simp_all)
-      done
-    with w  show False 
-      by (simp add: linorder_not_le [symmetric])
-  qed
-qed
-
-lemma add_right_mono: "a \<le> (b::'a::pordered_ab_semigroup_add) ==> a + c \<le> b + c"
+lemma add_right_mono:
+  "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   by (simp add: add_commute [of _ c] add_left_mono)
 
 text {* non-strict, in both arguments *}
 lemma add_mono:
-     "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::pordered_ab_semigroup_add)"
+  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   apply (erule add_right_mono [THEN order_trans])
   apply (simp add: add_commute add_left_mono)
   done
 
+end
+
+class pordered_cancel_ab_semigroup_add =
+  pordered_ab_semigroup_add + cancel_ab_semigroup_add
+begin
+
 lemma add_strict_left_mono:
-     "a < b ==> c + a < c + (b::'a::pordered_cancel_ab_semigroup_add)"
- by (simp add: order_less_le add_left_mono) 
+  "a < b \<Longrightarrow> c + a < c + b"
+  by (auto simp add: less_le add_left_mono)
 
 lemma add_strict_right_mono:
-     "a < b ==> a + c < b + (c::'a::pordered_cancel_ab_semigroup_add)"
- by (simp add: add_commute [of _ c] add_strict_left_mono)
+  "a < b \<Longrightarrow> a + c < b + c"
+  by (simp add: add_commute [of _ c] add_strict_left_mono)
 
 text{*Strict monotonicity in both arguments*}
-lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
-apply (erule add_strict_right_mono [THEN order_less_trans])
+lemma add_strict_mono:
+  "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
+apply (erule add_strict_right_mono [THEN less_trans])
 apply (erule add_strict_left_mono)
 done
 
 lemma add_less_le_mono:
-     "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
-apply (erule add_strict_right_mono [THEN order_less_le_trans])
-apply (erule add_left_mono) 
+  "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
+apply (erule add_strict_right_mono [THEN less_le_trans])
+apply (erule add_left_mono)
 done
 
 lemma add_le_less_mono:
-     "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"
-apply (erule add_right_mono [THEN order_le_less_trans])
+  "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
+apply (erule add_right_mono [THEN le_less_trans])
 apply (erule add_strict_left_mono) 
 done
 
+end
+
+class pordered_ab_semigroup_add_imp_le =
+  pordered_cancel_ab_semigroup_add +
+  assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
+begin
+
 lemma add_less_imp_less_left:
-      assumes less: "c + a < c + b"  shows "a < (b::'a::pordered_ab_semigroup_add_imp_le)"
+   assumes less: "c + a < c + b"
+   shows "a < b"
 proof -
   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   have "a <= b" 
@@ -317,30 +343,90 @@
 qed
 
 lemma add_less_imp_less_right:
-      "a + c < b + c ==> a < (b::'a::pordered_ab_semigroup_add_imp_le)"
+  "a + c < b + c \<Longrightarrow> a < b"
 apply (rule add_less_imp_less_left [of c])
 apply (simp add: add_commute)  
 done
 
 lemma add_less_cancel_left [simp]:
-    "(c+a < c+b) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"
-by (blast intro: add_less_imp_less_left add_strict_left_mono) 
+  "c + a < c + b \<longleftrightarrow> a < b"
+  by (blast intro: add_less_imp_less_left add_strict_left_mono) 
 
 lemma add_less_cancel_right [simp]:
-    "(a+c < b+c) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"
-by (blast intro: add_less_imp_less_right add_strict_right_mono)
+  "a + c < b + c \<longleftrightarrow> a < b"
+  by (blast intro: add_less_imp_less_right add_strict_right_mono)
 
 lemma add_le_cancel_left [simp]:
-    "(c+a \<le> c+b) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"
-by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
+  "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
+  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
 
 lemma add_le_cancel_right [simp]:
-    "(a+c \<le> b+c) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"
-by (simp add: add_commute[of a c] add_commute[of b c])
+  "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
+  by (simp add: add_commute [of a c] add_commute [of b c])
 
 lemma add_le_imp_le_right:
-      "a + c \<le> b + c ==> a \<le> (b::'a::pordered_ab_semigroup_add_imp_le)"
-by simp
+  "a + c \<le> b + c \<Longrightarrow> a \<le> b"
+  by simp
+
+end
+
+class pordered_ab_group_add =
+  ab_group_add + pordered_ab_semigroup_add
+begin
+
+subclass pordered_cancel_ab_semigroup_add
+  by unfold_locales
+
+subclass pordered_ab_semigroup_add_imp_le
+proof unfold_locales
+  fix a b c :: 'a
+  assume "c + a \<le> c + b"
+  hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
+  hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
+  thus "a \<le> b" by simp
+qed
+
+end
+
+class ordered_ab_semigroup_add =
+  linorder + pordered_ab_semigroup_add
+
+class ordered_cancel_ab_semigroup_add =
+  linorder + pordered_cancel_ab_semigroup_add
+
+subclass (in ordered_cancel_ab_semigroup_add) ordered_ab_semigroup_add
+  by unfold_locales
+
+subclass (in ordered_cancel_ab_semigroup_add) pordered_ab_semigroup_add_imp_le
+proof unfold_locales
+  fix a b c :: 'a
+  assume le: "c + a <= c + b"  
+  show "a <= b"
+  proof (rule ccontr)
+    assume w: "~ a \<le> b"
+    hence "b <= a" by (simp add: linorder_not_le)
+    hence le2: "c + b <= c + a" by (rule add_left_mono)
+    have "a = b" 
+      apply (insert le)
+      apply (insert le2)
+      apply (drule antisym, simp_all)
+      done
+    with w show False 
+      by (simp add: linorder_not_le [symmetric])
+  qed
+qed
+
+-- {* FIXME continue localization here *}
+
+lemma max_add_distrib_left:
+  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
+  shows  "(max x y) + z = max (x+z) (y+z)"
+by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
+
+lemma min_add_distrib_left:
+  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
+  shows  "(min x y) + z = min (x+z) (y+z)"
+by (rule min_of_mono [THEN sym], rule add_le_cancel_right)
 
 lemma add_increasing:
   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
@@ -362,16 +448,6 @@
   shows "[|0\<le>a; b<c|] ==> b < a + c"
 by (insert add_le_less_mono [of 0 a b c], simp)
 
-lemma max_add_distrib_left:
-  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
-  shows  "(max x y) + z = max (x+z) (y+z)"
-by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
-
-lemma min_add_distrib_left:
-  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
-  shows  "(min x y) + z = min (x+z) (y+z)"
-by (rule min_of_mono [THEN sym], rule add_le_cancel_right)
-
 lemma max_diff_distrib_left:
   fixes z :: "'a::pordered_ab_group_add"
   shows  "(max x y) - z = max (x-z) (y-z)"
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Orderings.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -14,10 +14,10 @@
 subsection {* Partial orders *}
 
 class order = ord +
-  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"
+  assumes less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+  and order_refl [iff]: "x \<le> x"
+  and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
+  assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
 
 begin
 
@@ -28,94 +28,94 @@
 
 text {* Reflexivity. *}
 
-lemma eq_refl: "x = y \<Longrightarrow> x \<^loc>\<le> y"
+lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
     -- {* This form is useful with the classical reasoner. *}
 by (erule ssubst) (rule order_refl)
 
-lemma less_irrefl [iff]: "\<not> x \<^loc>< x"
+lemma less_irrefl [iff]: "\<not> x < x"
 by (simp add: less_le)
 
-lemma le_less: "x \<^loc>\<le> y \<longleftrightarrow> x \<^loc>< y \<or> x = y"
+lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
     -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
 by (simp add: less_le) blast
 
-lemma le_imp_less_or_eq: "x \<^loc>\<le> y \<Longrightarrow> x \<^loc>< y \<or> x = y"
+lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
 unfolding less_le by blast
 
-lemma less_imp_le: "x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y"
+lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
 unfolding less_le by blast
 
-lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
+lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
 by (erule contrapos_pn, erule subst, rule less_irrefl)
 
 
 text {* Useful for simplification, but too risky to include by default. *}
 
-lemma less_imp_not_eq: "x \<^loc>< y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
+lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
 by auto
 
-lemma less_imp_not_eq2: "x \<^loc>< y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
+lemma less_imp_not_eq2: "x < y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
 by auto
 
 
 text {* Transitivity rules for calculational reasoning *}
 
-lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<^loc>\<le> b \<Longrightarrow> a \<^loc>< b"
+lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
 by (simp add: less_le)
 
-lemma le_neq_trans: "a \<^loc>\<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<^loc>< b"
+lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b"
 by (simp add: less_le)
 
 
 text {* Asymmetry. *}
 
-lemma less_not_sym: "x \<^loc>< y \<Longrightarrow> \<not> (y \<^loc>< x)"
+lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
 by (simp add: less_le antisym)
 
-lemma less_asym: "x \<^loc>< y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<^loc>< x) \<Longrightarrow> P"
+lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
 by (drule less_not_sym, erule contrapos_np) simp
 
-lemma eq_iff: "x = y \<longleftrightarrow> x \<^loc>\<le> y \<and> y \<^loc>\<le> x"
+lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
 by (blast intro: antisym)
 
-lemma antisym_conv: "y \<^loc>\<le> x \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
+lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
 by (blast intro: antisym)
 
-lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y"
+lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
 by (erule contrapos_pn, erule subst, rule less_irrefl)
 
 
 text {* Transitivity. *}
 
-lemma less_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
+lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
 by (simp add: less_le) (blast intro: order_trans antisym)
 
-lemma le_less_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z"
+lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
 by (simp add: less_le) (blast intro: order_trans antisym)
 
-lemma less_le_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>< z"
+lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
 by (simp add: less_le) (blast intro: order_trans antisym)
 
 
 text {* Useful for simplification, but too risky to include by default. *}
 
-lemma less_imp_not_less: "x \<^loc>< y \<Longrightarrow> (\<not> y \<^loc>< x) \<longleftrightarrow> True"
+lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
 by (blast elim: less_asym)
 
-lemma less_imp_triv: "x \<^loc>< y \<Longrightarrow> (y \<^loc>< x \<longrightarrow> P) \<longleftrightarrow> True"
+lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
 by (blast elim: less_asym)
 
 
 text {* Transitivity rules for calculational reasoning *}
 
-lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P"
+lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
 by (rule less_asym)
 
 
 text {* Reverse order *}
 
 lemma order_reverse:
-  "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+  "order (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
 by unfold_locales
    (simp add: less_le, auto intro: antisym order_trans)
 
@@ -128,67 +128,67 @@
   assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
 begin
 
-lemma less_linear: "x \<^loc>< y \<or> x = y \<or> y \<^loc>< x"
+lemma less_linear: "x < y \<or> x = y \<or> y < x"
 unfolding less_le using less_le linear by blast
 
-lemma le_less_linear: "x \<^loc>\<le> y \<or> y \<^loc>< x"
+lemma le_less_linear: "x \<le> y \<or> y < x"
 by (simp add: le_less less_linear)
 
 lemma le_cases [case_names le ge]:
-  "(x \<^loc>\<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>\<le> x \<Longrightarrow> P) \<Longrightarrow> P"
+  "(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
 using linear by blast
 
 lemma linorder_cases [case_names less equal greater]:
-  "(x \<^loc>< y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> P) \<Longrightarrow> P"
+  "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
 using less_linear by blast
 
-lemma not_less: "\<not> x \<^loc>< y \<longleftrightarrow> y \<^loc>\<le> x"
+lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
 apply (simp add: less_le)
 using linear apply (blast intro: antisym)
 done
 
 lemma not_less_iff_gr_or_eq:
- "\<not>(x \<^loc>< y) \<longleftrightarrow> (x \<^loc>> y | x = y)"
+ "\<not>(x < y) \<longleftrightarrow> (x > y | x = y)"
 apply(simp add:not_less le_less)
 apply blast
 done
 
-lemma not_le: "\<not> x \<^loc>\<le> y \<longleftrightarrow> y \<^loc>< x"
+lemma not_le: "\<not> x \<le> y \<longleftrightarrow> y < x"
 apply (simp add: less_le)
 using linear apply (blast intro: antisym)
 done
 
-lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<^loc>< y \<or> y \<^loc>< x"
+lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x < y \<or> y < x"
 by (cut_tac x = x and y = y in less_linear, auto)
 
-lemma neqE: "x \<noteq> y \<Longrightarrow> (x \<^loc>< y \<Longrightarrow> R) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> R) \<Longrightarrow> R"
+lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R"
 by (simp add: neq_iff) blast
 
-lemma antisym_conv1: "\<not> x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y"
+lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
 by (blast intro: antisym dest: not_less [THEN iffD1])
 
-lemma antisym_conv2: "x \<^loc>\<le> y \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
+lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
 by (blast intro: antisym dest: not_less [THEN iffD1])
 
-lemma antisym_conv3: "\<not> y \<^loc>< x \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y"
+lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
 by (blast intro: antisym dest: not_less [THEN iffD1])
 
 text{*Replacing the old Nat.leI*}
-lemma leI: "\<not> x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x"
+lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
 unfolding not_less .
 
-lemma leD: "y \<^loc>\<le> x \<Longrightarrow> \<not> x \<^loc>< y"
+lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
 unfolding not_less .
 
 (*FIXME inappropriate name (or delete altogether)*)
-lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y"
+lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y"
 unfolding not_le .
 
 
 text {* Reverse order *}
 
 lemma linorder_reverse:
-  "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+  "linorder (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)"
 by unfold_locales
   (simp add: less_le, auto intro: antisym order_trans simp add: linear)
 
@@ -199,42 +199,42 @@
 
 definition (in ord)
   min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  [code unfold, code inline del]: "min a b = (if a \<^loc>\<le> b then a else b)"
+  [code unfold, code inline del]: "min a b = (if a \<le> b then a else b)"
 
 definition (in ord)
   max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  [code unfold, code inline del]: "max a b = (if a \<^loc>\<le> b then b else a)"
+  [code unfold, code inline del]: "max a b = (if a \<le> b then b else a)"
 
 lemma min_le_iff_disj:
-  "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
+  "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
 unfolding min_def using linear by (auto intro: order_trans)
 
 lemma le_max_iff_disj:
-  "z \<^loc>\<le> max x y \<longleftrightarrow> z \<^loc>\<le> x \<or> z \<^loc>\<le> y"
+  "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
 unfolding max_def using linear by (auto intro: order_trans)
 
 lemma min_less_iff_disj:
-  "min x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<or> y \<^loc>< z"
+  "min x y < z \<longleftrightarrow> x < z \<or> y < z"
 unfolding min_def le_less using less_linear by (auto intro: less_trans)
 
 lemma less_max_iff_disj:
-  "z \<^loc>< max x y \<longleftrightarrow> z \<^loc>< x \<or> z \<^loc>< y"
+  "z < max x y \<longleftrightarrow> z < x \<or> z < y"
 unfolding max_def le_less using less_linear by (auto intro: less_trans)
 
 lemma min_less_iff_conj [simp]:
-  "z \<^loc>< min x y \<longleftrightarrow> z \<^loc>< x \<and> z \<^loc>< y"
+  "z < min x y \<longleftrightarrow> z < x \<and> z < y"
 unfolding min_def le_less using less_linear by (auto intro: less_trans)
 
 lemma max_less_iff_conj [simp]:
-  "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z"
+  "max x y < z \<longleftrightarrow> x < z \<and> y < z"
 unfolding max_def le_less using less_linear by (auto intro: less_trans)
 
 lemma split_min [noatp]:
-  "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)"
+  "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
 by (simp add: min_def)
 
 lemma split_max [noatp]:
-  "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)"
+  "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
 by (simp add: max_def)
 
 end
@@ -371,109 +371,109 @@
 (* The type constraint on @{term op =} below is necessary since the operation
    is not a parameter of the locale. *)
 lemmas (in order)
-  [order add less_reflE: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_reflE: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_irrefl [THEN notE]
 lemmas (in order)
-  [order add le_refl: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   order_refl
 lemmas (in order)
-  [order add less_imp_le: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_imp_le
 lemmas (in order)
-  [order add eqI: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   antisym
 lemmas (in order)
-  [order add eqD1: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   eq_refl
 lemmas (in order)
-  [order add eqD2: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   sym [THEN eq_refl]
 lemmas (in order)
-  [order add less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_trans
 lemmas (in order)
-  [order add less_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_le_trans
 lemmas (in order)
-  [order add le_less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   le_less_trans
 lemmas (in order)
-  [order add le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   order_trans
 lemmas (in order)
-  [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   le_neq_trans
 lemmas (in order)
-  [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   neq_le_trans
 lemmas (in order)
-  [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_imp_neq
 lemmas (in order)
-  [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
    eq_neq_eq_imp_neq
 lemmas (in order)
-  [order add not_sym: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] =
   not_sym
 
-lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = _
+lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _
 
 lemmas (in linorder)
-  [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_irrefl [THEN notE]
 lemmas (in linorder)
-  [order add le_refl: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   order_refl
 lemmas (in linorder)
-  [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_imp_le
 lemmas (in linorder)
-  [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   not_less [THEN iffD2]
 lemmas (in linorder)
-  [order add not_leI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   not_le [THEN iffD2]
 lemmas (in linorder)
-  [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   not_less [THEN iffD1]
 lemmas (in linorder)
-  [order add not_leD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   not_le [THEN iffD1]
 lemmas (in linorder)
-  [order add eqI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   antisym
 lemmas (in linorder)
-  [order add eqD1: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   eq_refl
 lemmas (in linorder)
-  [order add eqD2: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   sym [THEN eq_refl]
 lemmas (in linorder)
-  [order add less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_trans
 lemmas (in linorder)
-  [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_le_trans
 lemmas (in linorder)
-  [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   le_less_trans
 lemmas (in linorder)
-  [order add le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   order_trans
 lemmas (in linorder)
-  [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   le_neq_trans
 lemmas (in linorder)
-  [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   neq_le_trans
 lemmas (in linorder)
-  [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   less_imp_neq
 lemmas (in linorder)
-  [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   eq_neq_eq_imp_neq
 lemmas (in linorder)
-  [order add not_sym: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
+  [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] =
   not_sym
 
 
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Power.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -12,13 +12,13 @@
 begin
 
 class power = type +
-  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
+  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "^" 80)
 
 subsection{*Powers for Arbitrary Monoids*}
 
 class recpower = monoid_mult + power +
-  assumes power_0 [simp]: "a \<^loc>^ 0       = \<^loc>1"
-  assumes power_Suc:      "a \<^loc>^ Suc n = a \<^loc>* (a \<^loc>^ n)"
+  assumes power_0 [simp]: "a ^ 0       = 1"
+  assumes power_Suc:      "a ^ Suc n = a * (a ^ n)"
 
 lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
   by (simp add: power_Suc)
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -44,32 +44,28 @@
 subsection {* Real vector spaces *}
 
 class scaleR = type +
-  fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<^loc>*#" 75)
+  fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
 begin
 
 abbreviation
-  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "\<^loc>'/#" 70)
+  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "'/\<^sub>R" 70)
 where
-  "x \<^loc>/# r == scaleR (inverse r) x"
+  "x /\<^sub>R r == scaleR (inverse r) x"
 
 end
 
-notation (xsymbols)
-  scaleR (infixr "*\<^sub>R" 75) and
-  divideR (infixl "'/\<^sub>R" 70)
-
 instance real :: scaleR
   real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
 
 class real_vector = scaleR + ab_group_add +
-  assumes scaleR_right_distrib: "scaleR a (x \<^loc>+ y) = scaleR a x \<^loc>+ scaleR a y"
-  and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x \<^loc>+ scaleR b x"
+  assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
+  and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
   and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
   and scaleR_one [simp]: "scaleR 1 x = x"
 
 class real_algebra = real_vector + ring +
-  assumes mult_scaleR_left [simp]: "scaleR a x \<^loc>* y = scaleR a (x \<^loc>* y)"
-  and mult_scaleR_right [simp]: "x \<^loc>* scaleR a y = scaleR a (x \<^loc>* y)"
+  assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
+  and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
 
 class real_algebra_1 = real_algebra + ring_1
 
@@ -379,22 +375,22 @@
   real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
 
 class sgn_div_norm = scaleR + norm + sgn +
-  assumes sgn_div_norm: "sgn x = x \<^loc>/# norm x"
+  assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
 
 class real_normed_vector = real_vector + sgn_div_norm +
   assumes norm_ge_zero [simp]: "0 \<le> norm x"
-  and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = \<^loc>0"
-  and norm_triangle_ineq: "norm (x \<^loc>+ y) \<le> norm x + norm y"
+  and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
+  and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
   and norm_scaleR: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
 
 class real_normed_algebra = real_algebra + real_normed_vector +
-  assumes norm_mult_ineq: "norm (x \<^loc>* y) \<le> norm x * norm y"
+  assumes norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
 
 class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
-  assumes norm_one [simp]: "norm \<^loc>1 = 1"
+  assumes norm_one [simp]: "norm 1 = 1"
 
 class real_normed_div_algebra = real_div_algebra + real_normed_vector +
-  assumes norm_mult: "norm (x \<^loc>* y) = norm x * norm y"
+  assumes norm_mult: "norm (x * y) = norm x * norm y"
 
 class real_normed_field = real_field + real_normed_div_algebra
 
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -24,12 +24,12 @@
 *}
 
 class semiring = ab_semigroup_add + semigroup_mult +
-  assumes left_distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"
-  assumes right_distrib: "a \<^loc>* (b \<^loc>+ c) = a \<^loc>* b \<^loc>+ a \<^loc>* c"
+  assumes left_distrib: "(a + b) * c = a * c + b * c"
+  assumes right_distrib: "a * (b + c) = a * b + a * c"
 
 class mult_zero = times + zero +
-  assumes mult_zero_left [simp]: "\<^loc>0 \<^loc>* a = \<^loc>0"
-  assumes mult_zero_right [simp]: "a \<^loc>* \<^loc>0 = \<^loc>0"
+  assumes mult_zero_left [simp]: "0 * a = 0"
+  assumes mult_zero_right [simp]: "a * 0 = 0"
 
 class semiring_0 = semiring + comm_monoid_add + mult_zero
 
@@ -50,7 +50,7 @@
 qed
 
 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
-  assumes distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"
+  assumes distrib: "(a + b) * c = a * c + b * c"
 
 instance comm_semiring \<subseteq> semiring
 proof
@@ -73,7 +73,7 @@
 instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..
 
 class zero_neq_one = zero + one +
-  assumes zero_neq_one [simp]: "\<^loc>0 \<noteq> \<^loc>1"
+  assumes zero_neq_one [simp]: "0 \<noteq> 1"
 
 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
 
@@ -83,7 +83,7 @@
 instance comm_semiring_1 \<subseteq> semiring_1 ..
 
 class no_zero_divisors = zero + times +
-  assumes no_zero_divisors: "a \<noteq> \<^loc>0 \<Longrightarrow> b \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* b \<noteq> \<^loc>0"
+  assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 
 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
   + cancel_ab_semigroup_add + monoid_mult
@@ -131,8 +131,8 @@
 instance idom \<subseteq> ring_1_no_zero_divisors ..
 
 class division_ring = ring_1 + inverse +
-  assumes left_inverse [simp]:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
-  assumes right_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* inverse a = \<^loc>1"
+  assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
+  assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
 
 instance division_ring \<subseteq> ring_1_no_zero_divisors
 proof
@@ -153,8 +153,8 @@
 qed
 
 class field = comm_ring_1 + inverse +
-  assumes field_inverse:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
-  assumes divide_inverse: "a \<^loc>/ b = a \<^loc>* inverse b"
+  assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
+  assumes divide_inverse: "a / b = a * inverse b"
 
 instance field \<subseteq> division_ring
 proof
@@ -167,7 +167,7 @@
 instance field \<subseteq> idom ..
 
 class division_by_zero = zero + inverse +
-  assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0"
+  assumes inverse_zero [simp]: "inverse 0 = 0"
 
 
 subsection {* Distribution rules *}
@@ -211,8 +211,8 @@
 lemmas ring_simps = group_simps ring_distribs
 
 class mult_mono = times + zero + ord +
-  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"
+  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
+  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * 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 \<^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"
+  assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
+  assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
 
 instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
 
@@ -246,7 +246,7 @@
 qed
 
 class mult_mono1 = times + zero + ord +
-  assumes mult_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"
+  assumes mult_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * 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 \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"
+  assumes mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * 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 \<^loc>< \<^loc>0 then (uminus a) else a)"
+  assumes abs_if: "abs a = (if a < 0 then (uminus a) else a)"
 
 class sgn_if = sgn + zero + one + minus + ord +
-  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)"
+  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else uminus 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 \<^loc>< \<^loc>1"
+  assumes zero_less_one [simp]: "0 < 1"
 
 lemma pos_add_strict:
   fixes a b c :: "'a\<Colon>ordered_semidom"
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/SetInterval.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -16,36 +16,36 @@
 context ord
 begin
 definition
-  lessThan    :: "'a => 'a set"	("(1\<^loc>{..<_})") where
-  "\<^loc>{..<u} == {x. x \<^loc>< u}"
+  lessThan    :: "'a => 'a set"	("(1{..<_})") where
+  "{..<u} == {x. x < u}"
 
 definition
-  atMost      :: "'a => 'a set"	("(1\<^loc>{.._})") where
-  "\<^loc>{..u} == {x. x \<^loc>\<le> u}"
+  atMost      :: "'a => 'a set"	("(1{.._})") where
+  "{..u} == {x. x \<le> u}"
 
 definition
-  greaterThan :: "'a => 'a set"	("(1\<^loc>{_<..})") where
-  "\<^loc>{l<..} == {x. l\<^loc><x}"
+  greaterThan :: "'a => 'a set"	("(1{_<..})") where
+  "{l<..} == {x. l<x}"
 
 definition
-  atLeast     :: "'a => 'a set"	("(1\<^loc>{_..})") where
-  "\<^loc>{l..} == {x. l\<^loc>\<le>x}"
+  atLeast     :: "'a => 'a set"	("(1{_..})") where
+  "{l..} == {x. l\<le>x}"
 
 definition
-  greaterThanLessThan :: "'a => 'a => 'a set"  ("(1\<^loc>{_<..<_})") where
-  "\<^loc>{l<..<u} == \<^loc>{l<..} Int \<^loc>{..<u}"
+  greaterThanLessThan :: "'a => 'a => 'a set"  ("(1{_<..<_})") where
+  "{l<..<u} == {l<..} Int {..<u}"
 
 definition
-  atLeastLessThan :: "'a => 'a => 'a set"      ("(1\<^loc>{_..<_})") where
-  "\<^loc>{l..<u} == \<^loc>{l..} Int \<^loc>{..<u}"
+  atLeastLessThan :: "'a => 'a => 'a set"      ("(1{_..<_})") where
+  "{l..<u} == {l..} Int {..<u}"
 
 definition
-  greaterThanAtMost :: "'a => 'a => 'a set"    ("(1\<^loc>{_<.._})") where
-  "\<^loc>{l<..u} == \<^loc>{l<..} Int \<^loc>{..u}"
+  greaterThanAtMost :: "'a => 'a => 'a set"    ("(1{_<.._})") where
+  "{l<..u} == {l<..} Int {..u}"
 
 definition
-  atLeastAtMost :: "'a => 'a => 'a set"        ("(1\<^loc>{_.._})") where
-  "\<^loc>{l..u} == \<^loc>{l..} Int \<^loc>{..u}"
+  atLeastAtMost :: "'a => 'a => 'a set"        ("(1{_.._})") where
+  "{l..u} == {l..} Int {..u}"
 
 end
 (*
@@ -106,7 +106,7 @@
 
 subsection {* Various equivalences *}
 
-lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i\<^loc><k)"
+lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)"
 by (simp add: lessThan_def)
 
 lemma Compl_lessThan [simp]:
@@ -117,7 +117,7 @@
 lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
 by auto
 
-lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k\<^loc><i)"
+lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)"
 by (simp add: greaterThan_def)
 
 lemma Compl_greaterThan [simp]:
@@ -130,7 +130,7 @@
 apply (rule double_complement)
 done
 
-lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k\<^loc><=i)"
+lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)"
 by (simp add: atLeast_def)
 
 lemma Compl_atLeast [simp]:
@@ -138,7 +138,7 @@
 apply (simp add: lessThan_def atLeast_def le_def, auto)
 done
 
-lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i\<^loc><=k)"
+lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)"
 by (simp add: atMost_def)
 
 lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}"
@@ -194,19 +194,19 @@
 begin
 
 lemma greaterThanLessThan_iff [simp,noatp]:
-  "(i : \<^loc>{l<..<u}) = (l \<^loc>< i & i \<^loc>< u)"
+  "(i : {l<..<u}) = (l < i & i < u)"
 by (simp add: greaterThanLessThan_def)
 
 lemma atLeastLessThan_iff [simp,noatp]:
-  "(i : \<^loc>{l..<u}) = (l \<^loc><= i & i \<^loc>< u)"
+  "(i : {l..<u}) = (l <= i & i < u)"
 by (simp add: atLeastLessThan_def)
 
 lemma greaterThanAtMost_iff [simp,noatp]:
-  "(i : \<^loc>{l<..u}) = (l \<^loc>< i & i \<^loc><= u)"
+  "(i : {l<..u}) = (l < i & i <= u)"
 by (simp add: greaterThanAtMost_def)
 
 lemma atLeastAtMost_iff [simp,noatp]:
-  "(i : \<^loc>{l..u}) = (l \<^loc><= i & i \<^loc><= u)"
+  "(i : {l..u}) = (l <= i & i <= u)"
 by (simp add: atLeastAtMost_def)
 
 text {* The above four lemmas could be declared as iffs.
@@ -219,19 +219,19 @@
 context order
 begin
 
-lemma atLeastAtMost_empty [simp]: "n \<^loc>< m ==> \<^loc>{m..n} = {}";
+lemma atLeastAtMost_empty [simp]: "n < m ==> {m..n} = {}";
 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
 
-lemma atLeastLessThan_empty[simp]: "n \<^loc>\<le> m ==> \<^loc>{m..<n} = {}"
+lemma atLeastLessThan_empty[simp]: "n \<le> m ==> {m..<n} = {}"
 by (auto simp add: atLeastLessThan_def)
 
-lemma greaterThanAtMost_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}"
+lemma greaterThanAtMost_empty[simp]:"l \<le> k ==> {k<..l} = {}"
 by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
 
-lemma greaterThanLessThan_empty[simp]:"l \<^loc>\<le> k ==> \<^loc>{k<..l} = {}"
+lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..l} = {}"
 by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
 
-lemma atLeastAtMost_singleton [simp]: "\<^loc>{a..a} = {a}"
+lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
 by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
 
 end
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/Wellfounded_Relations.thy
--- a/src/HOL/Wellfounded_Relations.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/Wellfounded_Relations.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -113,15 +113,15 @@
 lemma (in linorder)
   finite_linorder_induct[consumes 1, case_names empty insert]:
  "finite A \<Longrightarrow> P {} \<Longrightarrow>
-  (!!A b. finite A \<Longrightarrow> ALL a:A. a \<^loc>< b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
+  (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
   \<Longrightarrow> P A"
 proof (induct A rule: measure_induct[where f=card])
   fix A :: "'a set"
   assume IH: "ALL B. card B < card A \<longrightarrow> finite B \<longrightarrow> P {} \<longrightarrow>
-                 (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a\<^loc><b) \<longrightarrow> P A \<longrightarrow> P (insert b A))
+                 (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a<b) \<longrightarrow> P A \<longrightarrow> P (insert b A))
                   \<longrightarrow> P B"
   and "finite A" and "P {}"
-  and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a \<^loc>< b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
+  and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
   show "P A"
   proof cases
     assume "A = {}" thus "P A" using `P {}` by simp
@@ -133,7 +133,7 @@
     note card_Diff1_less[OF `finite A` `Max A : A`]
     moreover have "finite ?B" using `finite A` by simp
     ultimately have "P ?B" using `P {}` step IH by blast
-    moreover have "\<forall>a\<in>?B. a \<^loc>< Max A"
+    moreover have "\<forall>a\<in>?B. a < Max A"
       using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp
     ultimately show "P A"
       using A insert_Diff_single step[OF `finite ?B`] by fastsimp
diff -r 250e1da3204b -r af5ef0d4d655 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy	Tue Oct 16 23:12:45 2007 +0200
@@ -9,8 +9,8 @@
 begin
 
 class semigroup = type +
-  fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
-  assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
+  fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
+  assumes assoc: "x \<otimes> y \<otimes> z = x \<otimes> (y \<otimes> z)"
 
 instance nat :: semigroup
   "m \<otimes> n \<equiv> m + n"
@@ -43,8 +43,8 @@
 qed
 
 class monoidl = semigroup +
-  fixes one :: 'a ("\<^loc>\<one>")
-  assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
+  fixes one :: 'a ("\<one>")
+  assumes neutl: "\<one> \<otimes> x = x"
 
 instance nat :: monoidl and int :: monoidl
   "\<one> \<equiv> 0"
@@ -74,66 +74,66 @@
 qed  
 
 class monoid = monoidl +
-  assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
+  assumes neutr: "x \<otimes> \<one> = x"
 begin
 
 definition
   units :: "'a set" where
-  "units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
+  "units = {y. \<exists>x. x \<otimes> y = \<one> \<and> y \<otimes> x = \<one>}"
 
 lemma inv_obtain:
   assumes "x \<in> units"
-  obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
+  obtains y where "y \<otimes> x = \<one>" and "x \<otimes> y = \<one>"
 proof -
   from assms units_def obtain y
-    where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
+    where "y \<otimes> x = \<one>" and "x \<otimes> y = \<one>" by auto
   thus ?thesis ..
 qed
 
 lemma inv_unique:
-  assumes "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
+  assumes "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>"
   shows "y = y'"
 proof -
-  from assms neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
-  also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
+  from assms neutr have "y = y \<otimes> (x \<otimes> y')" by simp
+  also with assoc have "... = (y \<otimes> x) \<otimes> y'" by simp
   also with assms neutl have "... = y'" by simp
   finally show ?thesis .
 qed
 
 lemma units_inv_comm:
-  assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
+  assumes inv: "x \<otimes> y = \<one>"
     and G: "x \<in> units"
-  shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
+  shows "y \<otimes> x = \<one>"
 proof -
   from G inv_obtain obtain z
-    where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast
-  from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp
-  with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp
+    where z_choice: "z \<otimes> x = \<one>" by blast
+  from inv neutl neutr have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by simp
+  with assoc have "z \<otimes> x \<otimes> y \<otimes> x = z \<otimes> x \<otimes> \<one>" by simp
   with neutl z_choice show ?thesis by simp
 qed
 
 fun
   npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
 where
-  "npow 0 x = \<^loc>\<one>"
-  | "npow (Suc n) x = x \<^loc>\<otimes> npow n x"
+  "npow 0 x = \<one>"
+  | "npow (Suc n) x = x \<otimes> npow n x"
 
 abbreviation
-  npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
-  "x \<^loc>\<up> n \<equiv> npow n x"
+  npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<up>" 75) where
+  "x \<up> n \<equiv> npow n x"
 
 lemma nat_pow_one:
-  "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
+  "\<one> \<up> n = \<one>"
 using neutl by (induct n) simp_all
 
-lemma nat_pow_mult: "x \<^loc>\<up> n \<^loc>\<otimes> x \<^loc>\<up> m = x \<^loc>\<up> (n + m)"
+lemma nat_pow_mult: "x \<up> n \<otimes> x \<up> m = x \<up> (n + m)"
 proof (induct n)
   case 0 with neutl show ?case by simp
 next
   case (Suc n) with Suc.hyps assoc show ?case by simp
 qed
 
-lemma nat_pow_pow: "(x \<^loc>\<up> m) \<^loc>\<up> n = x \<^loc>\<up> (n * m)"
+lemma nat_pow_pow: "(x \<up> m) \<up> n = x \<up> (n * m)"
 using nat_pow_mult by (induct n) simp_all
 
 end
@@ -153,7 +153,7 @@
 qed  
 
 class monoid_comm = monoid +
-  assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
+  assumes comm: "x \<otimes> y = y \<otimes> x"
 
 instance nat :: monoid_comm and int :: monoid_comm
 proof
@@ -174,30 +174,30 @@
 by default (simp_all add: split_paired_all mult_prod_def comm)
 
 class group = monoidl +
-  fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
-  assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
+  fixes inv :: "'a \<Rightarrow> 'a" ("\<div> _" [81] 80)
+  assumes invl: "\<div> x \<otimes> x = \<one>"
 begin
 
 lemma cancel:
-  "(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)"
+  "(x \<otimes> y = x \<otimes> z) = (y = z)"
 proof
   fix x y z :: 'a
-  assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
-  hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
-  with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp
+  assume eq: "x \<otimes> y = x \<otimes> z"
+  hence "\<div> x \<otimes> (x \<otimes> y) = \<div> x \<otimes> (x \<otimes> z)" by simp
+  with assoc have "\<div> x \<otimes> x \<otimes> y = \<div> x \<otimes> x \<otimes> z" by simp
   with neutl invl show "y = z" by simp
 next
   fix x y z :: 'a
   assume eq: "y = z"
-  thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
+  thus "x \<otimes> y = x \<otimes> z" by simp
 qed
 
 subclass monoid
 proof unfold_locales
   fix x
-  from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
-  with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp
-  with cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
+  from invl have "\<div> x \<otimes> x = \<one>" by simp
+  with assoc [symmetric] neutl invl have "\<div> x \<otimes> (x \<otimes> \<one>) = \<div> x \<otimes> x" by simp
+  with cancel show "x \<otimes> \<one> = x" by simp
 qed
 
 end context group begin
@@ -205,11 +205,11 @@
 find_theorems name: neut
 
 lemma invr:
-  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
+  "x \<otimes> \<div> x = \<one>"
 proof -
-  from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp
-  with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
-  with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
+  from neutl invl have "\<div> x \<otimes> x \<otimes> \<div> x = \<div> x" by simp
+  with neutr have "\<div> x \<otimes> x \<otimes> \<div> x = \<div> x \<otimes> \<one> " by simp
+  with assoc have "\<div> x \<otimes> (x \<otimes> \<div> x) = \<div> x \<otimes> \<one> " by simp
   with cancel show ?thesis ..
 qed
 
@@ -218,72 +218,72 @@
   unfolding units_def
 proof -
   fix x :: "'a"
-  from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" . 
-  then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" ..
-  hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast
-  thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}" by simp
+  from invl invr have "\<div> x \<otimes> x = \<one>" and "x \<otimes> \<div> x = \<one>" . 
+  then obtain y where "y \<otimes> x = \<one>" and "x \<otimes> y = \<one>" ..
+  hence "\<exists>y\<Colon>'a. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by blast
+  thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<otimes> y = \<one> \<and> y \<otimes> x = \<one>}" by simp
 qed
 
 lemma cancer:
-  "(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)"
+  "(y \<otimes> x = z \<otimes> x) = (y = z)"
 proof
-  assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x"
-  with assoc [symmetric] have "y \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = z \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x)" by (simp del: invr)
+  assume eq: "y \<otimes> x = z \<otimes> x"
+  with assoc [symmetric] have "y \<otimes> (x \<otimes> \<div> x) = z \<otimes> (x \<otimes> \<div> x)" by (simp del: invr)
   with invr neutr show "y = z" by simp
 next
   assume eq: "y = z"
-  thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp
+  thus "y \<otimes> x = z \<otimes> x" by simp
 qed
 
 lemma inv_one:
-  "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>"
+  "\<div> \<one> = \<one>"
 proof -
-  from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" ..
-  moreover from invr have "... = \<^loc>\<one>" by simp
+  from neutl have "\<div> \<one> = \<one> \<otimes> (\<div> \<one>)" ..
+  moreover from invr have "... = \<one>" by simp
   finally show ?thesis .
 qed
 
 lemma inv_inv:
-  "\<^loc>\<div> (\<^loc>\<div> x) = x"
+  "\<div> (\<div> x) = x"
 proof -
   from invl invr neutr
-    have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x" by simp
+    have "\<div> (\<div> x) \<otimes> \<div> x \<otimes> x = x \<otimes> \<div> x \<otimes> x" by simp
   with assoc [symmetric]
-    have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x) = x \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x)" by simp
+    have "\<div> (\<div> x) \<otimes> (\<div> x \<otimes> x) = x \<otimes> (\<div> x \<otimes> x)" by simp
   with invl neutr show ?thesis by simp
 qed
 
 lemma inv_mult_group:
-  "\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x"
+  "\<div> (x \<otimes> y) = \<div> y \<otimes> \<div> x"
 proof -
-  from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp
-  with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp
-  with neutl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
-  with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> (y \<^loc>\<otimes> \<^loc>\<div> y) \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
+  from invl have "\<div> (x \<otimes> y) \<otimes> (x \<otimes> y) = \<one>" by simp
+  with assoc have "\<div> (x \<otimes> y) \<otimes> x \<otimes> y = \<one>" by simp
+  with neutl have "\<div> (x \<otimes> y) \<otimes> x \<otimes> y \<otimes> \<div> y \<otimes> \<div> x = \<div> y \<otimes> \<div> x" by simp
+  with assoc have "\<div> (x \<otimes> y) \<otimes> (x \<otimes> (y \<otimes> \<div> y) \<otimes> \<div> x) = \<div> y \<otimes> \<div> x" by simp
   with invr neutr show ?thesis by simp
 qed
 
 lemma inv_comm:
-  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x"
+  "x \<otimes> \<div> x = \<div> x \<otimes> x"
 using invr invl by simp
 
 definition
   pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a"
 where
-  "pow k x = (if k < 0 then \<^loc>\<div> (npow (nat (-k)) x)
+  "pow k x = (if k < 0 then \<div> (npow (nat (-k)) x)
     else (npow (nat k) x))"
 
 abbreviation
-  pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>\<up>" 75)
+  pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<up>\<up>" 75)
 where
-  "x \<^loc>\<up>\<up> k \<equiv> pow k x"
+  "x \<up>\<up> k \<equiv> pow k x"
 
 lemma int_pow_zero:
-  "x \<^loc>\<up>\<up> (0\<Colon>int) = \<^loc>\<one>"
+  "x \<up>\<up> (0\<Colon>int) = \<one>"
 using pow_def by simp
 
 lemma int_pow_one:
-  "\<^loc>\<one> \<^loc>\<up>\<up> (k\<Colon>int) = \<^loc>\<one>"
+  "\<one> \<up>\<up> (k\<Colon>int) = \<one>"
 using pow_def nat_pow_one inv_one by simp
 
 end
diff -r 250e1da3204b -r af5ef0d4d655 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Oct 16 23:12:38 2007 +0200
+++ b/src/Pure/Isar/class.ML	Tue Oct 16 23:12:45 2007 +0200
@@ -7,7 +7,7 @@
 
 signature CLASS =
 sig
-  val fork_mixfix: bool -> bool -> mixfix -> mixfix * mixfix
+  val fork_mixfix: bool -> bool -> mixfix -> (mixfix * mixfix) * mixfix
 
   val axclass_cmd: bstring * xstring list
     -> ((bstring * Attrib.src list) * string list) list
@@ -19,9 +19,9 @@
   val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     -> xstring list -> theory -> string * Proof.context
   val init: class -> Proof.context -> Proof.context
-  val add_const_in_class: string -> (string * mixfix) * (string * term)
+  val add_const_in_class: string -> (string * mixfix) * term
     -> theory -> string * theory
-  val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term)
+  val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * term
     -> theory -> string * theory
   val remove_constraint: class -> string -> Proof.context -> Proof.context
   val is_class: theory -> class -> bool
@@ -54,13 +54,15 @@
 
 (** auxiliary **)
 
-fun fork_mixfix is_locale is_class mx =
-  let
-    val mx' = Syntax.unlocalize_mixfix mx;
-    val mx_global = if not is_locale orelse (is_class andalso not (mx = mx'))
-      then mx' else NoSyn;
-    val mx_local = if is_locale then mx else NoSyn;
-  in (mx_global, mx_local) end;
+val classN = "class";
+val introN = "intro";
+
+fun fork_mixfix false _ mx = ((NoSyn, NoSyn), mx)
+  | fork_mixfix true false mx = ((NoSyn, mx), NoSyn)
+  | fork_mixfix true true mx = ((mx, NoSyn), NoSyn);
+      (*let
+        val mx' = Syntax.unlocalize_mixfix mx;
+      in if mx' = mx then ((NoSyn, mx), NoSyn) else ((mx', mx), NoSyn) end;*)
 
 fun prove_interpretation tac prfx_atts expr inst =
   Locale.interpretation_i I prfx_atts expr inst
@@ -315,36 +317,36 @@
 datatype class_data = ClassData of {
   consts: (string * string) list
     (*locale parameter ~> constant name*),
-  local_sort: sort,
+  base_sort: sort,
   inst: (typ option list * term option list) * term Symtab.table
     (*canonical interpretation FIXME*),
+  morphism: morphism,
+    (*partial morphism of canonical interpretation*)
   intro: thm,
   defs: thm list,
-  operations: (string * (term * (typ * int))) list
-    (*constant name ~> (locale term, (constant constraint, instantiaton index of class typ))*),
-  operations_rev: (string * string) list
-    (*locale operation ~> constant name*)
+  operations: (string * ((term * typ) * (typ * int))) list
+    (*constant name ~> (locale term & typ,
+        (constant constraint, instantiaton index of class typ))*)
 };
 
 fun rep_class_data (ClassData d) = d;
-fun mk_class_data ((consts, local_sort, inst, intro),
-    (defs, operations, operations_rev)) =
-  ClassData { consts = consts, local_sort = local_sort, inst = inst,
-    intro = intro, defs = defs, operations = operations,
-    operations_rev = operations_rev };
-fun map_class_data f (ClassData { consts, local_sort, inst, intro,
-    defs, operations, operations_rev }) =
-  mk_class_data (f ((consts, local_sort, inst, intro),
-    (defs, operations, operations_rev)));
+fun mk_class_data ((consts, base_sort, inst, morphism, intro),
+    (defs, operations)) =
+  ClassData { consts = consts, base_sort = base_sort, inst = inst,
+    morphism = morphism, intro = intro, defs = defs,
+    operations = operations };
+fun map_class_data f (ClassData { consts, base_sort, inst, morphism, intro,
+    defs, operations }) =
+  mk_class_data (f ((consts, base_sort, inst, morphism, intro),
+    (defs, operations)));
 fun merge_class_data _ (ClassData { consts = consts,
-    local_sort = local_sort, inst = inst, intro = intro,
-    defs = defs1, operations = operations1, operations_rev = operations_rev1 },
-  ClassData { consts = _, local_sort = _, inst = _, intro = _,
-    defs = defs2, operations = operations2, operations_rev = operations_rev2 }) =
-  mk_class_data ((consts, local_sort, inst, intro),
+    base_sort = base_sort, inst = inst, morphism = morphism, intro = intro,
+    defs = defs1, operations = operations1 },
+  ClassData { consts = _, base_sort = _, inst = _, morphism = _, intro = _,
+    defs = defs2, operations = operations2 }) =
+  mk_class_data ((consts, base_sort, inst, morphism, intro),
     (Thm.merge_thms (defs1, defs2),
-      AList.merge (op =) (K true) (operations1, operations2),
-      AList.merge (op =) (K true) (operations_rev1, operations_rev2)));
+      AList.merge (op =) (K true) (operations1, operations2)));
 
 structure ClassData = TheoryDataFun
 (
@@ -381,6 +383,8 @@
 
 fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
 
+fun morphism thy = #morphism o the_class_data thy;
+
 fun these_intros thy =
   Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
     (ClassData.get thy) [];
@@ -388,26 +392,21 @@
 fun these_operations thy =
   maps (#operations o the_class_data thy) o ancestry thy;
 
-fun these_operations_rev thy =
-  maps (#operations_rev o the_class_data thy) o ancestry thy;
-
 fun local_operation thy = AList.lookup (op =) o these_operations thy;
 
-fun global_operation thy = AList.lookup (op =) o these_operations_rev thy;
-
-fun sups_local_sort thy sort =
+fun sups_base_sort thy sort =
   let
-    val sups = filter (is_some o lookup_class_data thy) sort
+    val sups = filter (is_class thy) sort
       |> Sign.minimize_sort thy;
-    val local_sort = case sups
-     of sup :: _ => #local_sort (the_class_data thy sup)
+    val base_sort = case sups
+     of _ :: _ => maps (#base_sort o the_class_data thy) sups
+          |> Sign.minimize_sort thy
       | [] => sort;
-  in (sups, local_sort) end;
+  in (sups, base_sort) end;
 
 fun print_classes thy =
   let
     val ctxt = ProofContext.init thy;
-
     val algebra = Sign.classes_of thy;
     val arities =
       Symtab.empty
@@ -422,11 +421,13 @@
     fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
       ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
     fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
-      (SOME o Pretty.str) ("class " ^ class ^ ":"),
+      (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
       (SOME o Pretty.block) [Pretty.str "supersort: ",
         (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
-      if is_class thy class then (SOME o Pretty.str) ("locale: " ^ class) else NONE,
-      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
+      if is_class thy class then (SOME o Pretty.str)
+        ("locale: " ^ Locale.extern thy class) else NONE,
+      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
+          (Pretty.str "parameters:" :: ps)) o map mk_param
         o these o Option.map #params o try (AxClass.get_info thy)) class,
       (SOME o Pretty.block o Pretty.breaks) [
         Pretty.str "instances:",
@@ -441,7 +442,7 @@
 
 (* updaters *)
 
-fun add_class_data ((class, superclasses), (cs, local_sort, inst, intro)) thy =
+fun add_class_data ((class, superclasses), (cs, base_sort, inst, phi, intro)) thy =
   let
     (*FIXME*)
     val is_empty = null (fold (fn ((_, ty), _) => fold_atyps cons ty) cs [])
@@ -453,26 +454,50 @@
         (Locale.parameters_of_expr thy (Locale.Locale class));
     val instT = if is_empty then [] else [SOME (TFree (Name.aT, [class]))];
     val inst' = ((instT, inst_params), inst);
-    val operations = map (fn (v_ty, (c, ty)) => (c, (Free v_ty, (ty, 0)))) cs;
+    val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
+      (c, ((Free v_ty, ty'), (Logic.varifyT ty, 0)))) cs;
     val cs = (map o pairself) fst cs;
     val add_class = Graph.new_node (class,
-        mk_class_data ((cs, local_sort, inst', intro), ([], operations, [])))
+        mk_class_data ((cs, base_sort, inst', phi, intro), ([], operations)))
       #> fold (curry Graph.add_edge class) superclasses;
   in
     ClassData.map add_class thy
   end;
 
-fun register_operation class (entry, some_def) =
-  (ClassData.map o Graph.map_node class o map_class_data o apsnd)
-    (fn (defs, operations, operations_rev) =>
-      (case some_def of NONE => defs | SOME def => def :: defs,
-        entry :: operations, (*FIXME*)operations_rev));
+fun register_operation class ((c, rhs), some_def) thy =
+  let
+    val ty = Sign.the_const_constraint thy c;
+    val typargs = Sign.const_typargs thy (c, ty);
+    val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
+    val ty' = Term.fastype_of rhs;
+  in
+    thy
+    |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
+      (fn (defs, operations) =>
+        (case some_def of NONE => defs | SOME def => def :: defs,
+          (c, ((rhs, ty'), (ty, typidx))) :: operations))
+  end;
 
 
 (** rule calculation, tactics and methods **)
 
 val class_prefix = Logic.const_of_class o Sign.base_name;
 
+fun calculate_morphism class cs =
+  let
+    val subst_typ = Term.map_type_tfree (fn var as (v, sort) =>
+      if v = Name.aT then TVar ((v, 0), [class]) else TVar ((v, 0), sort));
+    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
+         of SOME (c, _) => Const (c, ty)
+          | NONE => t)
+      | subst_aterm t = t;
+    val subst_term = map_aterms subst_aterm #> map_types subst_typ;
+  in
+    Morphism.identity
+    $> Morphism.term_morphism subst_term
+    $> Morphism.typ_morphism subst_typ
+  end;
+
 fun class_intro thy class sups =
   let
     fun class_elim class =
@@ -506,8 +531,6 @@
   let
     val params = these_params thy [class];
     val { inst = ((_, inst), _), ... } = the_class_data thy class;
-    (*val _ = tracing ("interpreting with " ^ cat_lines (map (setmp show_sorts true makestring)
-      (map_filter I inst)));*)
     val tac = ALLGOALS (ProofContext.fact_tac facts);
     val prfx = class_prefix class;
   in
@@ -548,82 +571,86 @@
 
 (* class context syntax *)
 
-fun internal_remove_constraint local_sort (c, (_, (ty, typidx))) ctxt =
+fun internal_remove_constraint base_sort (c, (_, (ty, _))) ctxt =
   let
-    val consts = ProofContext.consts_of ctxt;
-    val typargs = Consts.typargs consts (c, ty);
-    val typargs' = nth_map typidx (K (TVar ((Name.aT, 0), local_sort))) typargs;
-    val ty' = Consts.instance consts (c, typargs');
-  in ProofContext.add_const_constraint (c, SOME ty') ctxt end;
+    val ty' = ty
+      |> map_atyps (fn ty as TVar ((v, 0), _) =>
+           if v = Name.aT then TVar ((v, 0), base_sort) else ty)
+      |> SOME;
+  in ProofContext.add_const_constraint (c, ty') ctxt end;
 
 fun remove_constraint class c ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
+    val base_sort = (#base_sort o the_class_data thy) class;
     val SOME entry = local_operation thy [class] c;
   in
-    internal_remove_constraint
-      ((#local_sort o the_class_data thy) class) (c, entry) ctxt
+    internal_remove_constraint base_sort (c, entry) ctxt
   end;
 
-fun sort_term_check sups local_sort ts ctxt =
+fun sort_term_check sups base_sort ts ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
-    val local_operation = local_operation thy sups;
+    val local_operation = local_operation thy sups o fst;
+    val typargs = Consts.typargs (ProofContext.consts_of ctxt);
     val constraints = these_operations thy sups |> (map o apsnd) (fst o snd);
-    val consts = ProofContext.consts_of ctxt;
-    fun check_typ (c, ty) (t', idx) = case nth (Consts.typargs consts (c, ty)) idx
-     of TFree (v, _) => if v = Name.aT
-          then apfst (AList.update (op =) ((c, ty), t')) else I
-      | TVar (vi, _) => if TypeInfer.is_param vi
-          then apfst (AList.update (op =) ((c, ty), t'))
+    fun check_typ (c, ty) (TFree (v, _)) t = if v = Name.aT
+          then apfst (AList.update (op =) ((c, ty), t)) else I
+      | check_typ (c, ty) (TVar (vi, _)) t = if TypeInfer.is_param vi
+          then apfst (AList.update (op =) ((c, ty), t))
             #> apsnd (insert (op =) vi) else I
-      | _ => I;
-    fun add_const (Const (c, ty)) = (case local_operation c
-         of SOME (t', (_, idx)) => check_typ (c, ty) (t', idx)
-          | NONE => I)
+      | check_typ _ _ _ = I;
+    fun check_const (c, ty) ((t, _), (_, idx)) =
+      check_typ (c, ty) (nth (typargs (c, ty)) idx) t;
+    fun add_const (Const c_ty) = Option.map (check_const c_ty) (local_operation c_ty)
+          |> the_default I
       | add_const _ = I;
     val (cs, typarams) = (fold o fold_aterms) add_const ts ([], []);
-    val ts' = map (map_aterms
+    val subst_typ = map_type_tvar (fn var as (vi, _) =>
+      if member (op =) typarams vi then TFree (Name.aT, base_sort) else TVar var);
+    val subst_term = map_aterms
         (fn t as Const (c, ty) => the_default t (AList.lookup (op =) cs (c, ty)) | t => t)
-      #> (map_types o map_type_tvar) (fn var as (vi, _) => if member (op =) typarams vi
-           then TFree (Name.aT, local_sort) else TVar var)) ts;
+          #> map_types subst_typ;
+    val ts' = map subst_term ts;
     val ctxt' = fold (ProofContext.add_const_constraint o apsnd SOME) constraints ctxt;
   in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt') end;
 
-val uncheck = ref false;
+val uncheck = ref true;
 
 fun sort_term_uncheck sups ts ctxt =
   let
+    (*FIXME abbreviations*)
     val thy = ProofContext.theory_of ctxt;
-    val global_param = AList.lookup (op =) (these_params thy sups) #> Option.map fst;
-    val global_operation = global_operation thy sups;
-    fun globalize (t as Free (v, ty)) = (case global_param v
-         of SOME c => Const (c, ty)
-          | NONE => t)
-      | globalize (t as Const (c, ty)) = (case global_operation c
-         of SOME c => Const (c, ty)
-          | NONE => t)
-      | globalize t = t;
-    val ts' = if ! uncheck then (map o map_aterms) globalize ts else ts;
+    fun rew_app f (t1 $ t2) = rew_app f t1 $ f t2
+      | rew_app f t = t;
+    val rews = map (fn (c, ((t, ty), _)) => (t, Const (c, ty))) (these_operations thy sups);
+    val rews' = (map o apfst o rew_app) (Pattern.rewrite_term thy rews []) rews;
+    val _ = map (Thm.cterm_of thy o Logic.mk_equals) rews';
+    val ts' = if ! uncheck
+      then map (Pattern.rewrite_term thy rews' []) ts else ts;
   in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
 
-fun init_class_ctxt sups local_sort ctxt =
+fun init_class_ctxt sups base_sort ctxt =
   let
     val operations = these_operations (ProofContext.theory_of ctxt) sups;
+    fun standard_infer_types ts ctxt =
+      let
+        val ts' = ProofContext.standard_infer_types ctxt ts;
+      in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
   in
     ctxt
     |> Variable.declare_term
-        (Logic.mk_type (TFree (Name.aT, local_sort)))
-    |> fold (internal_remove_constraint local_sort) operations
-    |> Context.proof_map (Syntax.add_term_check 50 "class"
-        (sort_term_check sups local_sort)
-        #> Syntax.add_term_uncheck 50 "class"
-          (sort_term_uncheck sups))
+        (Logic.mk_type (TFree (Name.aT, base_sort)))
+    |> fold (internal_remove_constraint base_sort) operations
+    |> Context.proof_map (Syntax.add_term_check 1 "class"
+            (sort_term_check sups base_sort)
+        #> Syntax.add_term_check 1 "standard" standard_infer_types
+        #> Syntax.add_term_uncheck (~10) "class" (sort_term_uncheck sups))
   end;
 
 fun init class ctxt =
   init_class_ctxt [class]
-    ((#local_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
+    ((#base_sort o the_class_data (ProofContext.theory_of ctxt)) class) ctxt;
 
 
 (* class definition *)
@@ -633,7 +660,7 @@
 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, local_sort) = sups_local_sort thy supclasses;
+    val (sups, base_sort) = sups_base_sort thy supclasses;
     val supsort = Sign.minimize_sort thy supclasses;
     val suplocales = map Locale.Locale sups;
     val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
@@ -649,10 +676,10 @@
     ProofContext.init thy
     |> Locale.cert_expr supexpr [constrain]
     |> snd
-    |> init_class_ctxt sups local_sort
+    |> init_class_ctxt sups base_sort
     |> process_expr Locale.empty raw_elems
     |> fst
-    |> (fn elems => ((((sups, supconsts), (supsort, local_sort, mergeexpr)),
+    |> (fn elems => ((((sups, supconsts), (supsort, base_sort, mergeexpr)),
           (*FIXME*) if null includes then constrain :: elems else elems)))
   end;
 
@@ -688,26 +715,26 @@
     raw_supclasses raw_includes_elems raw_other_consts thy =
   let
     val class = Sign.full_name thy bname;
-    val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) =
+    val (((sups, supconsts), (supsort, base_sort, mergeexpr)), elems_syn) =
       prep_spec thy raw_supclasses raw_includes_elems;
     val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
     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;
+    fun fork_syntax (Element.Fixes xs) =
+          fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
+          #>> Element.Fixes
+      | fork_syntax x = pair x;
+    val (elems, global_syn) = fold_map fork_syntax elems_syn [];
+    fun globalize (c, ty) = 
+      ((c, Term.map_type_tfree (K (TFree (Name.aT, base_sort))) ty),
+        (the_default NoSyn o AList.lookup (op =) global_syn) c);
     fun extract_params thy =
       let
-        val params = Locale.parameters_of thy class;
-        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);
+        val params = map fst (Locale.parameters_of thy class);
       in
-        (map fst params, params
-        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (Name.aT, local_sort)))
-        |> (map o apsnd) (fork_mixfix true true #> fst)
-        |> chop (length supconsts)
-        |> snd)
+        (params, (map globalize o snd o chop (length supconsts)) params)
       end;
     fun extract_assumes params thy cs =
       let
@@ -722,28 +749,26 @@
         Locale.global_asms_of thy class
         |> map prep_asm
       end;
-    fun note_intro class_intro =
-      PureThy.note_thmss_qualified "" (class_prefix class)
-        [(("intro", []), [([class_intro], [])])]
-      #> snd
   in
     thy
     |> Locale.add_locale_i (SOME "") bname mergeexpr elems
     |> snd
     |> ProofContext.theory (`extract_params
-      #-> (fn (globals, params) =>
+      #-> (fn (all_params, params) =>
         define_class_params (bname, supsort) params
           (extract_assumes params) other_consts
       #-> (fn (_, (consts, axioms)) =>
         `(fn thy => class_intro thy class sups)
       #-> (fn class_intro =>
+        PureThy.note_thmss_qualified "" (NameSpace.append class classN)
+          [((introN, []), [([class_intro], [])])]
+      #-> (fn [(_, [class_intro])] =>
         add_class_data ((class, sups),
-          (map fst params ~~ consts, local_sort,
-            mk_inst class (map fst globals) (map snd supconsts @ consts),
-              class_intro))
-      #> note_intro class_intro
+          (map fst params ~~ consts, base_sort,
+            mk_inst class (map fst all_params) (map snd supconsts @ consts),
+              calculate_morphism class (supconsts @ (map (fst o fst) params ~~ consts)), class_intro))
       #> class_interpretation class axioms []
-      ))))
+      )))))
     |> pair class
   end;
 
@@ -757,56 +782,29 @@
 
 (* definition in class target *)
 
-fun export_fixes thy class =
+fun add_const_in_class class ((c, mx), rhs) thy =
   let
-    val cs = these_params thy [class];
-    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) cs v
-         of SOME (c, _) => Const (c, ty)
-          | NONE => t)
-      | subst_aterm t = t;
-  in Term.map_aterms subst_aterm end;
-
-fun mk_operation_entry thy (c, rhs) =
-  let
-    val ty = Logic.unvarifyT (Sign.the_const_constraint thy c);
-    val typargs = Sign.const_typargs thy (c, ty);
-    val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
-  in (c, (rhs, (ty, typidx))) end;
-
-fun add_const_in_class class ((c, mx), (c_loc, rhs)) thy =
-  let
-    val _ = tracing c_loc;
     val prfx = class_prefix class;
     val thy' = thy |> Sign.add_path prfx;
+    val phi = morphism thy' class;
 
-    val rhs' = export_fixes thy' class rhs;
-    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
-      if w = Name.aT then TFree (w, [class]) else TFree var);
+    val c' = Sign.full_name thy' c;
+    val ((mx', _), _) = fork_mixfix true true mx;
+    val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
     val ty' = Term.fastype_of rhs';
-    val ty'' = subst_typ ty';
-    val c' = Sign.full_name thy' c;
-    val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
     val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
-    val (mx', _) = fork_mixfix true true mx;
-    fun interpret def thy =
-      let
-        val def' = symmetric def;
-        val def_eq = (map_types Logic.unvarifyT o Thm.prop_of) def';
-      in
-        thy
-        |> class_interpretation class [def'] [def_eq]
-        |> Sign.add_const_constraint (c', SOME ty'')
-        |> `(fn thy => mk_operation_entry thy (c', rhs))
-        |-> (fn entry => register_operation class (entry, SOME def'))
-      end;
+    val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
   in
     thy'
     |> Sign.hide_consts_i false [c'']
     |> Sign.declare_const [] (c, ty', mx') |> snd
     |> Sign.parent_path
     |> Sign.sticky_prefix prfx
-    |> PureThy.add_defs_i false [(def, [])]
-    |-> (fn [def] => interpret def)
+    |> yield_singleton (PureThy.add_defs_i false) (def, [])
+    |>> Thm.symmetric
+    |-> (fn def => class_interpretation class [def]
+                [(map_types Logic.unvarifyT o Thm.prop_of) def]
+          #> register_operation class ((c', rhs), SOME def))
     |> Sign.restore_naming thy
     |> pair c'
   end;
@@ -814,20 +812,20 @@
 
 (* abbreviation in class target *)
 
-fun add_abbrev_in_class class prmode ((c, mx), (c_loc, rhs)) thy =
+fun add_abbrev_in_class class prmode ((c, mx), rhs) thy =
   let
-    val _ = tracing c_loc;
     val prfx = class_prefix class;
+    val phi = morphism thy class;
+
     val naming = Sign.naming_of thy |> NameSpace.add_path prfx |> NameSpace.add_path prfx;
       (*FIXME*)
     val c' = NameSpace.full naming c;
-    val rhs' = export_fixes thy class rhs;
+    val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
     val ty' = Term.fastype_of rhs';
-    val entry = mk_operation_entry thy (c', rhs);
   in
     thy
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
-    |> register_operation class (entry, NONE)
+    |> register_operation class ((c', rhs), NONE)
     |> pair c'
   end;