proper syntax during class specification
authorhaftmann
Sat Sep 29 08:58:51 2007 +0200 (2007-09-29 ago)
changeset 24748ee0a0eb6b738
parent 24747 6ded9235c2b6
child 24749 151b3758f576
proper syntax during class specification
src/HOL/Dense_Linear_Order.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/HOL.thy
src/HOL/Library/Kleene_Algebras.thy
src/HOL/List.thy
src/HOL/OrderedGroup.thy
src/HOL/Orderings.thy
src/HOL/Real/RealVector.thy
src/HOL/Ring_and_Field.thy
src/HOL/SetInterval.thy
src/Pure/Isar/class.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/HOL/Dense_Linear_Order.thy	Fri Sep 28 10:35:53 2007 +0200
     1.2 +++ b/src/HOL/Dense_Linear_Order.thy	Sat Sep 29 08:58:51 2007 +0200
     1.3 @@ -22,153 +22,153 @@
     1.4  context linorder
     1.5  begin
     1.6  
     1.7 -lemma less_not_permute: "\<not> (x \<sqsubset> y \<and> y \<sqsubset> x)" by (simp add: not_less linear)
     1.8 +lemma less_not_permute: "\<not> (x \<^loc>< y \<and> y \<^loc>< x)" by (simp add: not_less linear)
     1.9  
    1.10  lemma gather_simps: 
    1.11    shows 
    1.12 -  "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> x \<sqsubset> u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> (insert u U). x \<sqsubset> y) \<and> P x)"
    1.13 -  and "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> l \<sqsubset> x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> P x)"
    1.14 -  "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> x \<sqsubset> u) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> (insert u U). x \<sqsubset> y))"
    1.15 -  and "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y) \<and> l \<sqsubset> x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y))"  by auto
    1.16 +  "(\<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)"
    1.17 +  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)"
    1.18 +  "(\<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))"
    1.19 +  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
    1.20  
    1.21  lemma 
    1.22 -  gather_start: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y\<in> {}. x \<sqsubset> y) \<and> P x)" 
    1.23 +  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)" 
    1.24    by simp
    1.25  
    1.26 -text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
    1.27 -lemma minf_lt:  "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubset> t \<longleftrightarrow> True)" by auto
    1.28 -lemma minf_gt: "\<exists>z . \<forall>x. x \<sqsubset> z \<longrightarrow>  (t \<sqsubset> x \<longleftrightarrow>  False)"
    1.29 +text{* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
    1.30 +lemma minf_lt:  "\<exists>z . \<forall>x. x \<^loc>< z \<longrightarrow> (x \<^loc>< t \<longleftrightarrow> True)" by auto
    1.31 +lemma minf_gt: "\<exists>z . \<forall>x. x \<^loc>< z \<longrightarrow>  (t \<^loc>< x \<longleftrightarrow>  False)"
    1.32    by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    1.33  
    1.34 -lemma minf_le: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<sqsubseteq> t \<longleftrightarrow> True)" by (auto simp add: less_le)
    1.35 -lemma minf_ge: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (t \<sqsubseteq> x \<longleftrightarrow> False)"
    1.36 +lemma minf_le: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x \<^loc>\<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
    1.37 +lemma minf_ge: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (t \<^loc>\<le> x \<longleftrightarrow> False)"
    1.38    by (auto simp add: less_le not_less not_le)
    1.39 -lemma minf_eq: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    1.40 -lemma minf_neq: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    1.41 -lemma minf_P: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    1.42 +lemma minf_eq: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    1.43 +lemma minf_neq: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    1.44 +lemma minf_P: "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    1.45  
    1.46 -text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
    1.47 -lemma pinf_gt:  "\<exists>z . \<forall>x. z \<sqsubset> x \<longrightarrow> (t \<sqsubset> x \<longleftrightarrow> True)" by auto
    1.48 -lemma pinf_lt: "\<exists>z . \<forall>x. z \<sqsubset> x \<longrightarrow>  (x \<sqsubset> t \<longleftrightarrow>  False)"
    1.49 +text{* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
    1.50 +lemma pinf_gt:  "\<exists>z . \<forall>x. z \<^loc>< x \<longrightarrow> (t \<^loc>< x \<longleftrightarrow> True)" by auto
    1.51 +lemma pinf_lt: "\<exists>z . \<forall>x. z \<^loc>< x \<longrightarrow>  (x \<^loc>< t \<longleftrightarrow>  False)"
    1.52    by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
    1.53  
    1.54 -lemma pinf_ge: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (t \<sqsubseteq> x \<longleftrightarrow> True)" by (auto simp add: less_le)
    1.55 -lemma pinf_le: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x \<sqsubseteq> t \<longleftrightarrow> False)"
    1.56 +lemma pinf_ge: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (t \<^loc>\<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
    1.57 +lemma pinf_le: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x \<^loc>\<le> t \<longleftrightarrow> False)"
    1.58    by (auto simp add: less_le not_less not_le)
    1.59 -lemma pinf_eq: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    1.60 -lemma pinf_neq: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    1.61 -lemma pinf_P: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    1.62 +lemma pinf_eq: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
    1.63 +lemma pinf_neq: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
    1.64 +lemma pinf_P: "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
    1.65  
    1.66 -lemma nmi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<sqsubset> t \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
    1.67 -lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t \<sqsubset> x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)"
    1.68 +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
    1.69 +lemma nmi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t \<^loc>< x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)"
    1.70    by (auto simp add: le_less)
    1.71 -lemma  nmi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<sqsubseteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
    1.72 -lemma  nmi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<sqsubseteq> x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
    1.73 -lemma  nmi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
    1.74 -lemma  nmi_neq: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
    1.75 -lemma  nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
    1.76 -lemma  nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x) ;
    1.77 -  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)\<rbrakk> \<Longrightarrow>
    1.78 -  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
    1.79 -lemma  nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x) ;
    1.80 -  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)\<rbrakk> \<Longrightarrow>
    1.81 -  \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<sqsubseteq> x)" by auto
    1.82 +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
    1.83 +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
    1.84 +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
    1.85 +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
    1.86 +lemma  nmi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
    1.87 +lemma  nmi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x) ;
    1.88 +  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)\<rbrakk> \<Longrightarrow>
    1.89 +  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
    1.90 +lemma  nmi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x) ;
    1.91 +  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)\<rbrakk> \<Longrightarrow>
    1.92 +  \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. u \<^loc>\<le> x)" by auto
    1.93  
    1.94 -lemma  npi_lt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<sqsubset> t \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by (auto simp add: le_less)
    1.95 -lemma  npi_gt: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<sqsubset> x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
    1.96 -lemma  npi_le: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x \<sqsubseteq> t \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
    1.97 -lemma  npi_ge: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<sqsubseteq> x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
    1.98 -lemma  npi_eq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and>  x = t \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
    1.99 -lemma  npi_neq: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u )" by auto
   1.100 -lemma  npi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
   1.101 -lemma  npi_conj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u) ;  \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk>
   1.102 -  \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
   1.103 -lemma  npi_disj: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk>
   1.104 -  \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<sqsubseteq> u)" by auto
   1.105 +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)
   1.106 +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
   1.107 +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
   1.108 +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
   1.109 +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
   1.110 +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
   1.111 +lemma  npi_P: "\<forall> x. ~P \<and> P \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
   1.112 +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>
   1.113 +  \<Longrightarrow>  \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
   1.114 +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>
   1.115 +  \<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow>  (\<exists> u\<in> U. x \<^loc>\<le> u)" by auto
   1.116  
   1.117 -lemma lin_dense_lt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> x \<sqsubset> t \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y \<sqsubset> t)"
   1.118 +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)"
   1.119  proof(clarsimp)
   1.120 -  fix x l u y  assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x"
   1.121 -    and xu: "x\<sqsubset>u"  and px: "x \<sqsubset> t" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
   1.122 +  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"
   1.123 +    and xu: "x\<^loc><u"  and px: "x \<^loc>< t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
   1.124    from tU noU ly yu have tny: "t\<noteq>y" by auto
   1.125 -  {assume H: "t \<sqsubset> y"
   1.126 +  {assume H: "t \<^loc>< y"
   1.127      from less_trans[OF lx px] less_trans[OF H yu]
   1.128 -    have "l \<sqsubset> t \<and> t \<sqsubset> u"  by simp
   1.129 +    have "l \<^loc>< t \<and> t \<^loc>< u"  by simp
   1.130      with tU noU have "False" by auto}
   1.131 -  hence "\<not> t \<sqsubset> y"  by auto hence "y \<sqsubseteq> t" by (simp add: not_less)
   1.132 -  thus "y \<sqsubset> t" using tny by (simp add: less_le)
   1.133 +  hence "\<not> t \<^loc>< y"  by auto hence "y \<^loc>\<le> t" by (simp add: not_less)
   1.134 +  thus "y \<^loc>< t" using tny by (simp add: less_le)
   1.135  qed
   1.136  
   1.137 -lemma lin_dense_gt: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l \<sqsubset> x \<and> x \<sqsubset> u \<and> t \<sqsubset> x \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> t \<sqsubset> y)"
   1.138 +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)"
   1.139  proof(clarsimp)
   1.140    fix x l u y
   1.141 -  assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x" and xu: "x\<sqsubset>u"
   1.142 -  and px: "t \<sqsubset> x" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
   1.143 +  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"
   1.144 +  and px: "t \<^loc>< x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
   1.145    from tU noU ly yu have tny: "t\<noteq>y" by auto
   1.146 -  {assume H: "y\<sqsubset> t"
   1.147 -    from less_trans[OF ly H] less_trans[OF px xu] have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
   1.148 +  {assume H: "y\<^loc>< t"
   1.149 +    from less_trans[OF ly H] less_trans[OF px xu] have "l \<^loc>< t \<and> t \<^loc>< u" by simp
   1.150      with tU noU have "False" by auto}
   1.151 -  hence "\<not> y\<sqsubset>t"  by auto hence "t \<sqsubseteq> y" by (auto simp add: not_less)
   1.152 -  thus "t \<sqsubset> y" using tny by (simp add:less_le)
   1.153 +  hence "\<not> y\<^loc><t"  by auto hence "t \<^loc>\<le> y" by (auto simp add: not_less)
   1.154 +  thus "t \<^loc>< y" using tny by (simp add:less_le)
   1.155  qed
   1.156  
   1.157 -lemma lin_dense_le: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> x \<sqsubseteq> t \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y\<sqsubseteq> t)"
   1.158 +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)"
   1.159  proof(clarsimp)
   1.160    fix x l u y
   1.161 -  assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x" and xu: "x\<sqsubset>u"
   1.162 -  and px: "x \<sqsubseteq> t" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
   1.163 +  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"
   1.164 +  and px: "x \<^loc>\<le> t" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
   1.165    from tU noU ly yu have tny: "t\<noteq>y" by auto
   1.166 -  {assume H: "t \<sqsubset> y"
   1.167 +  {assume H: "t \<^loc>< y"
   1.168      from less_le_trans[OF lx px] less_trans[OF H yu]
   1.169 -    have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
   1.170 +    have "l \<^loc>< t \<and> t \<^loc>< u" by simp
   1.171      with tU noU have "False" by auto}
   1.172 -  hence "\<not> t \<sqsubset> y"  by auto thus "y \<sqsubseteq> t" by (simp add: not_less)
   1.173 +  hence "\<not> t \<^loc>< y"  by auto thus "y \<^loc>\<le> t" by (simp add: not_less)
   1.174  qed
   1.175  
   1.176 -lemma lin_dense_ge: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> t \<sqsubseteq> x \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> t \<sqsubseteq> y)"
   1.177 +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)"
   1.178  proof(clarsimp)
   1.179    fix x l u y
   1.180 -  assume tU: "t \<in> U" and noU: "\<forall>t. l \<sqsubset> t \<and> t \<sqsubset> u \<longrightarrow> t \<notin> U" and lx: "l \<sqsubset> x" and xu: "x\<sqsubset>u"
   1.181 -  and px: "t \<sqsubseteq> x" and ly: "l\<sqsubset>y" and yu:"y \<sqsubset> u"
   1.182 +  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"
   1.183 +  and px: "t \<^loc>\<le> x" and ly: "l\<^loc><y" and yu:"y \<^loc>< u"
   1.184    from tU noU ly yu have tny: "t\<noteq>y" by auto
   1.185 -  {assume H: "y\<sqsubset> t"
   1.186 +  {assume H: "y\<^loc>< t"
   1.187      from less_trans[OF ly H] le_less_trans[OF px xu]
   1.188 -    have "l \<sqsubset> t \<and> t \<sqsubset> u" by simp
   1.189 +    have "l \<^loc>< t \<and> t \<^loc>< u" by simp
   1.190      with tU noU have "False" by auto}
   1.191 -  hence "\<not> y\<sqsubset>t"  by auto thus "t \<sqsubseteq> y" by (simp add: not_less)
   1.192 +  hence "\<not> y\<^loc><t"  by auto thus "t \<^loc>\<le> y" by (simp add: not_less)
   1.193  qed
   1.194 -lemma lin_dense_eq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> x = t   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y= t)"  by auto
   1.195 -lemma lin_dense_neq: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> x \<noteq> t   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> y\<noteq> t)"  by auto
   1.196 -lemma lin_dense_P: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P)"  by auto
   1.197 +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
   1.198 +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
   1.199 +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
   1.200  
   1.201  lemma lin_dense_conj:
   1.202 -  "\<lbrakk>\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P1 x
   1.203 -  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P1 y) ;
   1.204 -  \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P2 x
   1.205 -  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
   1.206 -  \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> (P1 x \<and> P2 x)
   1.207 -  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> (P1 y \<and> P2 y))"
   1.208 +  "\<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
   1.209 +  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ;
   1.210 +  \<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
   1.211 +  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
   1.212 +  \<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)
   1.213 +  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<and> P2 y))"
   1.214    by blast
   1.215  lemma lin_dense_disj:
   1.216 -  "\<lbrakk>\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P1 x
   1.217 -  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P1 y) ;
   1.218 -  \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P2 x
   1.219 -  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
   1.220 -  \<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> (P1 x \<or> P2 x)
   1.221 -  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> (P1 y \<or> P2 y))"
   1.222 +  "\<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
   1.223 +  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P1 y) ;
   1.224 +  \<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
   1.225 +  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P2 y)\<rbrakk> \<Longrightarrow>
   1.226 +  \<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)
   1.227 +  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> (P1 y \<or> P2 y))"
   1.228    by blast
   1.229  
   1.230 -lemma npmibnd: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)\<rbrakk>
   1.231 -  \<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')"
   1.232 +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>
   1.233 +  \<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')"
   1.234  by auto
   1.235  
   1.236  lemma finite_set_intervals:
   1.237 -  assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S"
   1.238 -  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<sqsubseteq> x" and Su: "\<forall> x\<in> S. x \<sqsubseteq> u"
   1.239 -  shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S) \<and> a \<sqsubseteq> x \<and> x \<sqsubseteq> b \<and> P x"
   1.240 +  assumes px: "P x" and lx: "l \<^loc>\<le> x" and xu: "x \<^loc>\<le> u" and linS: "l\<in> S"
   1.241 +  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"
   1.242 +  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"
   1.243  proof-
   1.244 -  let ?Mx = "{y. y\<in> S \<and> y \<sqsubseteq> x}"
   1.245 -  let ?xM = "{y. y\<in> S \<and> x \<sqsubseteq> y}"
   1.246 +  let ?Mx = "{y. y\<in> S \<and> y \<^loc>\<le> x}"
   1.247 +  let ?xM = "{y. y\<in> S \<and> x \<^loc>\<le> y}"
   1.248    let ?a = "Max ?Mx"
   1.249    let ?b = "Min ?xM"
   1.250    have MxS: "?Mx \<subseteq> S" by blast
   1.251 @@ -179,31 +179,31 @@
   1.252    hence fxM: "finite ?xM" using fS finite_subset by auto
   1.253    from xu uinS have linxM: "u \<in> ?xM" by blast
   1.254    hence xMne: "?xM \<noteq> {}" by blast
   1.255 -  have ax:"?a \<sqsubseteq> x" using Mxne fMx by auto
   1.256 -  have xb:"x \<sqsubseteq> ?b" using xMne fxM by auto
   1.257 +  have ax:"?a \<^loc>\<le> x" using Mxne fMx by auto
   1.258 +  have xb:"x \<^loc>\<le> ?b" using xMne fxM by auto
   1.259    have "?a \<in> ?Mx" using Max_in[OF fMx Mxne] by simp hence ainS: "?a \<in> S" using MxS by blast
   1.260    have "?b \<in> ?xM" using Min_in[OF fxM xMne] by simp hence binS: "?b \<in> S" using xMS by blast
   1.261 -  have noy:"\<forall> y. ?a \<sqsubset> y \<and> y \<sqsubset> ?b \<longrightarrow> y \<notin> S"
   1.262 +  have noy:"\<forall> y. ?a \<^loc>< y \<and> y \<^loc>< ?b \<longrightarrow> y \<notin> S"
   1.263    proof(clarsimp)
   1.264 -    fix y   assume ay: "?a \<sqsubset> y" and yb: "y \<sqsubset> ?b" and yS: "y \<in> S"
   1.265 +    fix y   assume ay: "?a \<^loc>< y" and yb: "y \<^loc>< ?b" and yS: "y \<in> S"
   1.266      from yS have "y\<in> ?Mx \<or> y\<in> ?xM" by (auto simp add: linear)
   1.267 -    moreover {assume "y \<in> ?Mx" hence "y \<sqsubseteq> ?a" using Mxne fMx by auto with ay have "False" by (simp add: not_le[symmetric])}
   1.268 -    moreover {assume "y \<in> ?xM" hence "?b \<sqsubseteq> y" using xMne fxM by auto with yb have "False" by (simp add: not_le[symmetric])}
   1.269 +    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])}
   1.270 +    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])}
   1.271      ultimately show "False" by blast
   1.272    qed
   1.273    from ainS binS noy ax xb px show ?thesis by blast
   1.274  qed
   1.275  
   1.276  lemma finite_set_intervals2:
   1.277 -  assumes px: "P x" and lx: "l \<sqsubseteq> x" and xu: "x \<sqsubseteq> u" and linS: "l\<in> S"
   1.278 -  and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<sqsubseteq> x" and Su: "\<forall> x\<in> S. x \<sqsubseteq> u"
   1.279 -  shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S) \<and> a \<sqsubset> x \<and> x \<sqsubset> b \<and> P x)"
   1.280 +  assumes px: "P x" and lx: "l \<^loc>\<le> x" and xu: "x \<^loc>\<le> u" and linS: "l\<in> S"
   1.281 +  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"
   1.282 +  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)"
   1.283  proof-
   1.284    from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
   1.285    obtain a and b where
   1.286 -    as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a \<sqsubset> y \<and> y \<sqsubset> b \<longrightarrow> y \<notin> S"
   1.287 -    and axb: "a \<sqsubseteq> x \<and> x \<sqsubseteq> b \<and> P x"  by auto
   1.288 -  from axb have "x= a \<or> x= b \<or> (a \<sqsubset> x \<and> x \<sqsubset> b)" by (auto simp add: le_less)
   1.289 +    as: "a\<in> S" and bs: "b\<in> S" and noS:"\<forall>y. a \<^loc>< y \<and> y \<^loc>< b \<longrightarrow> y \<notin> S"
   1.290 +    and axb: "a \<^loc>\<le> x \<and> x \<^loc>\<le> b \<and> P x"  by auto
   1.291 +  from axb have "x= a \<or> x= b \<or> (a \<^loc>< x \<and> x \<^loc>< b)" by (auto simp add: le_less)
   1.292    thus ?thesis using px as bs noS by blast
   1.293  qed
   1.294  
   1.295 @@ -216,44 +216,44 @@
   1.296  
   1.297  lemma dlo_qe_bnds: 
   1.298    assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
   1.299 -  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l \<sqsubset> u)"
   1.300 +  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)"
   1.301  proof (simp only: atomize_eq, rule iffI)
   1.302    assume H: "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)"
   1.303    then obtain x where xL: "\<forall>y\<in>L. y \<^loc>< x" and xU: "\<forall>y\<in>U. x \<^loc>< y" by blast
   1.304    {fix l u assume l: "l \<in> L" and u: "u \<in> U"
   1.305      from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]]
   1.306 -    have "l \<sqsubset> u" .}
   1.307 +    have "l \<^loc>< u" .}
   1.308    thus "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u" by blast
   1.309  next
   1.310    assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l \<^loc>< u"
   1.311    let ?ML = "Max L"
   1.312    let ?MU = "Min U"  
   1.313 -  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<sqsubseteq> ?ML" by auto
   1.314 -  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<sqsubseteq> u" by auto
   1.315 -  from th1 th2 H have "?ML \<sqsubset> ?MU" by auto
   1.316 -  with dense obtain w where th3: "?ML \<sqsubset> w" and th4: "w \<sqsubset> ?MU" by blast
   1.317 -  from th3 th1' have "\<forall>l \<in> L. l \<sqsubset> w" by auto
   1.318 -  moreover from th4 th2' have "\<forall>u \<in> U. w \<sqsubset> u" by auto
   1.319 +  from fL ne have th1: "?ML \<in> L" and th1': "\<forall>l\<in>L. l \<^loc>\<le> ?ML" by auto
   1.320 +  from fU neU have th2: "?MU \<in> U" and th2': "\<forall>u\<in>U. ?MU \<^loc>\<le> u" by auto
   1.321 +  from th1 th2 H have "?ML \<^loc>< ?MU" by auto
   1.322 +  with dense obtain w where th3: "?ML \<^loc>< w" and th4: "w \<^loc>< ?MU" by blast
   1.323 +  from th3 th1' have "\<forall>l \<in> L. l \<^loc>< w" by auto
   1.324 +  moreover from th4 th2' have "\<forall>u \<in> U. w \<^loc>< u" by auto
   1.325    ultimately show "\<exists>x. (\<forall>y\<in>L. y \<^loc>< x) \<and> (\<forall>y\<in>U. x \<^loc>< y)" by auto
   1.326  qed
   1.327  
   1.328  lemma dlo_qe_noub: 
   1.329    assumes ne: "L \<noteq> {}" and fL: "finite L"
   1.330 -  shows "(\<exists>x. (\<forall>y \<in> L. y \<sqsubset> x) \<and> (\<forall>y \<in> {}. x \<sqsubset> y)) \<equiv> True"
   1.331 +  shows "(\<exists>x. (\<forall>y \<in> L. y \<^loc>< x) \<and> (\<forall>y \<in> {}. x \<^loc>< y)) \<equiv> True"
   1.332  proof(simp add: atomize_eq)
   1.333 -  from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<sqsubset> M" by blast
   1.334 -  from ne fL have "\<forall>x \<in> L. x \<sqsubseteq> Max L" by simp
   1.335 -  with M have "\<forall>x\<in>L. x \<sqsubset> M" by (auto intro: le_less_trans)
   1.336 +  from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L \<^loc>< M" by blast
   1.337 +  from ne fL have "\<forall>x \<in> L. x \<^loc>\<le> Max L" by simp
   1.338 +  with M have "\<forall>x\<in>L. x \<^loc>< M" by (auto intro: le_less_trans)
   1.339    thus "\<exists>x. \<forall>y\<in>L. y \<^loc>< x" by blast
   1.340  qed
   1.341  
   1.342  lemma dlo_qe_nolb: 
   1.343    assumes ne: "U \<noteq> {}" and fU: "finite U"
   1.344 -  shows "(\<exists>x. (\<forall>y \<in> {}. y \<sqsubset> x) \<and> (\<forall>y \<in> U. x \<sqsubset> y)) \<equiv> True"
   1.345 +  shows "(\<exists>x. (\<forall>y \<in> {}. y \<^loc>< x) \<and> (\<forall>y \<in> U. x \<^loc>< y)) \<equiv> True"
   1.346  proof(simp add: atomize_eq)
   1.347 -  from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<sqsubset> Min U" by blast
   1.348 -  from ne fU have "\<forall>x \<in> U. Min U \<sqsubseteq> x" by simp
   1.349 -  with M have "\<forall>x\<in>U. M \<sqsubset> x" by (auto intro: less_le_trans)
   1.350 +  from lt_ex[rule_format, of "Min U"] obtain M where M: "M \<^loc>< Min U" by blast
   1.351 +  from ne fU have "\<forall>x \<in> U. Min U \<^loc>\<le> x" by simp
   1.352 +  with M have "\<forall>x\<in>U. M \<^loc>< x" by (auto intro: less_le_trans)
   1.353    thus "\<exists>x. \<forall>y\<in>U. x \<^loc>< y" by blast
   1.354  qed
   1.355  
   1.356 @@ -263,9 +263,12 @@
   1.357  lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
   1.358    le_less neq_iff linear less_not_permute
   1.359  
   1.360 -lemma axiom: "dense_linear_order (op \<sqsubseteq>) (op \<sqsubset>)" .
   1.361 -lemma atoms: includes meta_term_syntax
   1.362 -  shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
   1.363 +lemma axiom: "dense_linear_order (op \<^loc>\<le>) (op \<^loc><)" .
   1.364 +lemma atoms:
   1.365 +  includes meta_term_syntax
   1.366 +  shows "TERM (less :: 'a \<Rightarrow> _)"
   1.367 +    and "TERM (less_eq :: 'a \<Rightarrow> _)"
   1.368 +    and "TERM (op = :: 'a \<Rightarrow> _)" .
   1.369  
   1.370  declare axiom[langford qe: dlo_qe_bnds dlo_qe_nolb dlo_qe_noub gather: gather_start gather_simps atoms: atoms]
   1.371  declare dlo_simps[langfordsimp]
   1.372 @@ -300,22 +303,22 @@
   1.373  text {* Linear order without upper bounds *}
   1.374  
   1.375  class linorder_no_ub = linorder +
   1.376 -  assumes gt_ex: "\<exists>y. x \<sqsubset> y"
   1.377 +  assumes gt_ex: "\<exists>y. x \<^loc>< y"
   1.378  begin
   1.379  
   1.380 -lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
   1.381 +lemma ge_ex: "\<exists>y. x \<^loc>\<le> y" using gt_ex by auto
   1.382  
   1.383 -text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
   1.384 +text {* Theorems for @{text "\<exists>z. \<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
   1.385  lemma pinf_conj:
   1.386 -  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.387 -  and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   1.388 -  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
   1.389 +  assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.390 +  and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   1.391 +  shows "\<exists>z. \<forall>x. z \<^loc><  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
   1.392  proof-
   1.393 -  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.394 -     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   1.395 -  from gt_ex obtain z where z:"max z1 z2 \<sqsubset> z" by blast
   1.396 -  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
   1.397 -  {fix x assume H: "z \<sqsubset> x"
   1.398 +  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.399 +     and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   1.400 +  from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast
   1.401 +  from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all
   1.402 +  {fix x assume H: "z \<^loc>< x"
   1.403      from less_trans[OF zz1 H] less_trans[OF zz2 H]
   1.404      have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')"  using z1 zz1 z2 zz2 by auto
   1.405    }
   1.406 @@ -323,25 +326,25 @@
   1.407  qed
   1.408  
   1.409  lemma pinf_disj:
   1.410 -  assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.411 -  and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   1.412 -  shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
   1.413 +  assumes ex1: "\<exists>z1. \<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.414 +  and ex2: "\<exists>z2. \<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   1.415 +  shows "\<exists>z. \<forall>x. z \<^loc><  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
   1.416  proof-
   1.417 -  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.418 -     and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   1.419 -  from gt_ex obtain z where z:"max z1 z2 \<sqsubset> z" by blast
   1.420 -  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z" by simp_all
   1.421 -  {fix x assume H: "z \<sqsubset> x"
   1.422 +  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. z1 \<^loc>< x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.423 +     and z2: "\<forall>x. z2 \<^loc>< x \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   1.424 +  from gt_ex obtain z where z:"max z1 z2 \<^loc>< z" by blast
   1.425 +  from z have zz1: "z1 \<^loc>< z" and zz2: "z2 \<^loc>< z" by simp_all
   1.426 +  {fix x assume H: "z \<^loc>< x"
   1.427      from less_trans[OF zz1 H] less_trans[OF zz2 H]
   1.428      have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')"  using z1 zz1 z2 zz2 by auto
   1.429    }
   1.430    thus ?thesis by blast
   1.431  qed
   1.432  
   1.433 -lemma pinf_ex: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
   1.434 +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"
   1.435  proof-
   1.436 -  from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   1.437 -  from gt_ex obtain x where x: "z \<sqsubset> x" by blast
   1.438 +  from ex obtain z where z: "\<forall>x. z \<^loc>< x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   1.439 +  from gt_ex obtain x where x: "z \<^loc>< x" by blast
   1.440    from z x p1 show ?thesis by blast
   1.441  qed
   1.442  
   1.443 @@ -350,22 +353,22 @@
   1.444  text {* Linear order without upper bounds *}
   1.445  
   1.446  class linorder_no_lb = linorder +
   1.447 -  assumes lt_ex: "\<exists>y. y \<sqsubset> x"
   1.448 +  assumes lt_ex: "\<exists>y. y \<^loc>< x"
   1.449  begin
   1.450  
   1.451 -lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
   1.452 +lemma le_ex: "\<exists>y. y \<^loc>\<le> x" using lt_ex by auto
   1.453  
   1.454  
   1.455 -text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
   1.456 +text {* Theorems for @{text "\<exists>z. \<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
   1.457  lemma minf_conj:
   1.458 -  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.459 -  and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   1.460 -  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
   1.461 +  assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.462 +  and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   1.463 +  shows "\<exists>z. \<forall>x. x \<^loc><  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
   1.464  proof-
   1.465 -  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   1.466 -  from lt_ex obtain z where z:"z \<sqsubset> min z1 z2" by blast
   1.467 -  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
   1.468 -  {fix x assume H: "x \<sqsubset> z"
   1.469 +  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
   1.470 +  from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast
   1.471 +  from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all
   1.472 +  {fix x assume H: "x \<^loc>< z"
   1.473      from less_trans[OF H zz1] less_trans[OF H zz2]
   1.474      have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')"  using z1 zz1 z2 zz2 by auto
   1.475    }
   1.476 @@ -373,24 +376,24 @@
   1.477  qed
   1.478  
   1.479  lemma minf_disj:
   1.480 -  assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.481 -  and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   1.482 -  shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
   1.483 +  assumes ex1: "\<exists>z1. \<forall>x. x \<^loc>< z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
   1.484 +  and ex2: "\<exists>z2. \<forall>x. x \<^loc>< z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   1.485 +  shows "\<exists>z. \<forall>x. x \<^loc><  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
   1.486  proof-
   1.487 -  from ex1 ex2 obtain z1 and z2 where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')" by blast
   1.488 -  from lt_ex obtain z where z:"z \<sqsubset> min z1 z2" by blast
   1.489 -  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2" by simp_all
   1.490 -  {fix x assume H: "x \<sqsubset> z"
   1.491 +  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
   1.492 +  from lt_ex obtain z where z:"z \<^loc>< min z1 z2" by blast
   1.493 +  from z have zz1: "z \<^loc>< z1" and zz2: "z \<^loc>< z2" by simp_all
   1.494 +  {fix x assume H: "x \<^loc>< z"
   1.495      from less_trans[OF H zz1] less_trans[OF H zz2]
   1.496      have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')"  using z1 zz1 z2 zz2 by auto
   1.497    }
   1.498    thus ?thesis by blast
   1.499  qed
   1.500  
   1.501 -lemma minf_ex: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
   1.502 +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"
   1.503  proof-
   1.504 -  from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   1.505 -  from lt_ex obtain x where x: "x \<sqsubset> z" by blast
   1.506 +  from ex obtain z where z: "\<forall>x. x \<^loc>< z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
   1.507 +  from lt_ex obtain x where x: "x \<^loc>< z" by blast
   1.508    from z x p1 show ?thesis by blast
   1.509  qed
   1.510  
   1.511 @@ -399,7 +402,7 @@
   1.512  
   1.513  class constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
   1.514    fixes between
   1.515 -  assumes between_less: "x \<sqsubset> y \<Longrightarrow> x \<sqsubset> between x y \<and> between x y \<sqsubset> y"
   1.516 +  assumes between_less: "x \<^loc>< y \<Longrightarrow> x \<^loc>< between x y \<and> between x y \<^loc>< y"
   1.517       and  between_same: "between x x = x"
   1.518  
   1.519  instance advanced constr_dense_linear_order < dense_linear_order
   1.520 @@ -416,41 +419,41 @@
   1.521  
   1.522  lemma rinf_U:
   1.523    assumes fU: "finite U"
   1.524 -  and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
   1.525 -  \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
   1.526 -  and nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')"
   1.527 +  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
   1.528 +  \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )"
   1.529 +  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')"
   1.530    and nmi: "\<not> MP"  and npi: "\<not> PP"  and ex: "\<exists> x.  P x"
   1.531    shows "\<exists> u\<in> U. \<exists> u' \<in> U. P (between u u')"
   1.532  proof-
   1.533    from ex obtain x where px: "P x" by blast
   1.534 -  from px nmi npi nmpiU have "\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'" by auto
   1.535 -  then obtain u and u' where uU:"u\<in> U" and uU': "u' \<in> U" and ux:"u \<sqsubseteq> x" and xu':"x \<sqsubseteq> u'" by auto
   1.536 +  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
   1.537 +  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
   1.538    from uU have Une: "U \<noteq> {}" by auto
   1.539    let ?l = "Min U"
   1.540    let ?u = "Max U"
   1.541    have linM: "?l \<in> U" using fU Une by simp
   1.542    have uinM: "?u \<in> U" using fU Une by simp
   1.543 -  have lM: "\<forall> t\<in> U. ?l \<sqsubseteq> t" using Une fU by auto
   1.544 -  have Mu: "\<forall> t\<in> U. t \<sqsubseteq> ?u" using Une fU by auto
   1.545 -  have th:"?l \<sqsubseteq> u" using uU Une lM by auto
   1.546 -  from order_trans[OF th ux] have lx: "?l \<sqsubseteq> x" .
   1.547 -  have th: "u' \<sqsubseteq> ?u" using uU' Une Mu by simp
   1.548 -  from order_trans[OF xu' th] have xu: "x \<sqsubseteq> ?u" .
   1.549 +  have lM: "\<forall> t\<in> U. ?l \<^loc>\<le> t" using Une fU by auto
   1.550 +  have Mu: "\<forall> t\<in> U. t \<^loc>\<le> ?u" using Une fU by auto
   1.551 +  have th:"?l \<^loc>\<le> u" using uU Une lM by auto
   1.552 +  from order_trans[OF th ux] have lx: "?l \<^loc>\<le> x" .
   1.553 +  have th: "u' \<^loc>\<le> ?u" using uU' Une Mu by simp
   1.554 +  from order_trans[OF xu' th] have xu: "x \<^loc>\<le> ?u" .
   1.555    from finite_set_intervals2[where P="P",OF px lx xu linM uinM fU lM Mu]
   1.556    have "(\<exists> s\<in> U. P s) \<or>
   1.557 -      (\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x)" .
   1.558 +      (\<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)" .
   1.559    moreover { fix u assume um: "u\<in>U" and pu: "P u"
   1.560      have "between u u = u" by (simp add: between_same)
   1.561      with um pu have "P (between u u)" by simp
   1.562      with um have ?thesis by blast}
   1.563    moreover{
   1.564 -    assume "\<exists> t1\<in> U. \<exists> t2 \<in> U. (\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U) \<and> t1 \<sqsubset> x \<and> x \<sqsubset> t2 \<and> P x"
   1.565 +    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"
   1.566        then obtain t1 and t2 where t1M: "t1 \<in> U" and t2M: "t2\<in> U"
   1.567 -        and noM: "\<forall> y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U" and t1x: "t1 \<sqsubset> x" and xt2: "x \<sqsubset> t2" and px: "P x"
   1.568 +        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"
   1.569          by blast
   1.570 -      from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" .
   1.571 +      from less_trans[OF t1x xt2] have t1t2: "t1 \<^loc>< t2" .
   1.572        let ?u = "between t1 t2"
   1.573 -      from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto
   1.574 +      from between_less t1t2 have t1lu: "t1 \<^loc>< ?u" and ut2: "?u \<^loc>< t2" by auto
   1.575        from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast
   1.576        with t1M t2M have ?thesis by blast}
   1.577      ultimately show ?thesis by blast
   1.578 @@ -458,11 +461,11 @@
   1.579  
   1.580  theorem fr_eq:
   1.581    assumes fU: "finite U"
   1.582 -  and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
   1.583 -   \<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
   1.584 -  and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<sqsubseteq> x)"
   1.585 -  and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<sqsubseteq> u)"
   1.586 -  and mi: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x = MP)"  and pi: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x = PP)"
   1.587 +  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
   1.588 +   \<longrightarrow> (\<forall> y. l \<^loc>< y \<and> y \<^loc>< u \<longrightarrow> P y )"
   1.589 +  and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<^loc>\<le> x)"
   1.590 +  and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<^loc>\<le> u)"
   1.591 +  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)"
   1.592    shows "(\<exists> x. P x) \<equiv> (MP \<or> PP \<or> (\<exists> u \<in> U. \<exists> u'\<in> U. P (between u u')))"
   1.593    (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D")
   1.594  proof-
   1.595 @@ -472,7 +475,7 @@
   1.596     moreover {assume "MP \<or> PP" hence "?D" by blast}
   1.597     moreover {assume nmi: "\<not> MP" and npi: "\<not> PP"
   1.598       from npmibnd[OF nmibnd npibnd]
   1.599 -     have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')" .
   1.600 +     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')" .
   1.601       from rinf_U[OF fU lin_dense nmpiU nmi npi px] have "?D" by blast}
   1.602     ultimately have "?D" by blast}
   1.603   moreover
   1.604 @@ -492,8 +495,11 @@
   1.605  lemmas lin_dense_thms = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P
   1.606  
   1.607  lemma ferrack_axiom: "constr_dense_linear_order less_eq less between" by fact
   1.608 -lemma atoms: includes meta_term_syntax
   1.609 -  shows "TERM (op \<sqsubset> :: 'a \<Rightarrow> _)" and "TERM (op \<sqsubseteq>)" and "TERM (op = :: 'a \<Rightarrow> _)" .
   1.610 +lemma atoms:
   1.611 +  includes meta_term_syntax
   1.612 +  shows "TERM (less :: 'a \<Rightarrow> _)"
   1.613 +    and "TERM (less_eq :: 'a \<Rightarrow> _)"
   1.614 +    and "TERM (op = :: 'a \<Rightarrow> _)" .
   1.615  
   1.616  declare ferrack_axiom [ferrack minf: minf_thms pinf: pinf_thms
   1.617      nmi: nmi_thms npi: npi_thms lindense:
   1.618 @@ -504,7 +510,7 @@
   1.619  fun simps phi = map (Morphism.thm phi) [@{thm "not_less"}, @{thm "not_le"}]
   1.620  fun generic_whatis phi =
   1.621   let
   1.622 -  val [lt, le] = map (Morphism.term phi) [@{term "op \<sqsubset>"}, @{term "op \<sqsubseteq>"}]
   1.623 +  val [lt, le] = map (Morphism.term phi) [@{term "op \<^loc><"}, @{term "op \<^loc>\<le>"}]
   1.624    fun h x t =
   1.625     case term_of t of
   1.626       Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
     2.1 --- a/src/HOL/Divides.thy	Fri Sep 28 10:35:53 2007 +0200
     2.2 +++ b/src/HOL/Divides.thy	Sat Sep 29 08:58:51 2007 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4    [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
     2.5  
     2.6  class dvd_mod = times + div + zero + -- {* for code generation *}
     2.7 -  assumes dvd_def_mod [code func]: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
     2.8 +  assumes dvd_def_mod [code func]: "x \<^loc>dvd y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
     2.9  
    2.10  definition
    2.11    quorem :: "(nat*nat) * (nat*nat) => bool" where
    2.12 @@ -880,8 +880,6 @@
    2.13  qed
    2.14  
    2.15  
    2.16 -
    2.17 -
    2.18  subsection {* Code generation for div, mod and dvd on nat *}
    2.19  
    2.20  definition [code func del]:
     3.1 --- a/src/HOL/Finite_Set.thy	Fri Sep 28 10:35:53 2007 +0200
     3.2 +++ b/src/HOL/Finite_Set.thy	Sat Sep 29 08:58:51 2007 +0200
     3.3 @@ -2006,8 +2006,8 @@
     3.4  subsubsection{* Semi-Lattices *}
     3.5  
     3.6  locale ACIfSL = ord + ACIf +
     3.7 -  assumes below_def: "x \<sqsubseteq> y \<longleftrightarrow> x \<cdot> y = x"
     3.8 -  and strict_below_def: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
     3.9 +  assumes below_def: "less_eq x y \<longleftrightarrow> x \<cdot> y = x"
    3.10 +  and strict_below_def: "less x y \<longleftrightarrow> less_eq x y \<and> x \<noteq> y"
    3.11  begin
    3.12  
    3.13  lemma below_refl [simp]: "x \<^loc>\<le> x"
    3.14 @@ -2033,9 +2033,9 @@
    3.15    then show ?thesis by (simp add: below_def)
    3.16  qed
    3.17  
    3.18 -lemma below_f_conv [simp,noatp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    3.19 +lemma below_f_conv [simp,noatp]: "x \<^loc>\<le> y \<cdot> z = (x \<^loc>\<le> y \<and> x \<^loc>\<le> z)"
    3.20  proof
    3.21 -  assume "x \<sqsubseteq> y \<cdot> z"
    3.22 +  assume "x \<^loc>\<le> y \<cdot> z"
    3.23    hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
    3.24    have "x \<cdot> y = x"
    3.25    proof -
    3.26 @@ -2051,14 +2051,14 @@
    3.27      also have "\<dots> = x" by(rule xyzx)
    3.28      finally show ?thesis .
    3.29    qed
    3.30 -  ultimately show "x \<sqsubseteq> y \<and> x \<sqsubseteq> z" by(simp add: below_def)
    3.31 +  ultimately show "x \<^loc>\<le> y \<and> x \<^loc>\<le> z" by(simp add: below_def)
    3.32  next
    3.33 -  assume a: "x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
    3.34 +  assume a: "x \<^loc>\<le> y \<and> x \<^loc>\<le> z"
    3.35    hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
    3.36    have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
    3.37    also have "x \<cdot> y = x" using a by(simp_all add: below_def)
    3.38    also have "x \<cdot> z = x" using a by(simp_all add: below_def)
    3.39 -  finally show "x \<sqsubseteq> y \<cdot> z" by(simp_all add: below_def)
    3.40 +  finally show "x \<^loc>\<le> y \<cdot> z" by(simp_all add: below_def)
    3.41  qed
    3.42  
    3.43  end
    3.44 @@ -2072,38 +2072,38 @@
    3.45  begin
    3.46  
    3.47  lemma above_f_conv:
    3.48 - "x \<cdot> y \<sqsubseteq> z = (x \<sqsubseteq> z \<or> y \<sqsubseteq> z)"
    3.49 + "x \<cdot> y \<^loc>\<le> z = (x \<^loc>\<le> z \<or> y \<^loc>\<le> z)"
    3.50  proof
    3.51 -  assume a: "x \<cdot> y \<sqsubseteq> z"
    3.52 +  assume a: "x \<cdot> y \<^loc>\<le> z"
    3.53    have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
    3.54 -  thus "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
    3.55 +  thus "x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
    3.56    proof
    3.57 -    assume "x \<cdot> y = x" hence "x \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
    3.58 +    assume "x \<cdot> y = x" hence "x \<^loc>\<le> z" by(rule subst)(rule a) thus ?thesis ..
    3.59    next
    3.60 -    assume "x \<cdot> y = y" hence "y \<sqsubseteq> z" by(rule subst)(rule a) thus ?thesis ..
    3.61 +    assume "x \<cdot> y = y" hence "y \<^loc>\<le> z" by(rule subst)(rule a) thus ?thesis ..
    3.62    qed
    3.63  next
    3.64 -  assume "x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
    3.65 -  thus "x \<cdot> y \<sqsubseteq> z"
    3.66 +  assume "x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
    3.67 +  thus "x \<cdot> y \<^loc>\<le> z"
    3.68    proof
    3.69 -    assume a: "x \<sqsubseteq> z"
    3.70 +    assume a: "x \<^loc>\<le> z"
    3.71      have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
    3.72      also have "x \<cdot> z = x" using a by(simp add:below_def)
    3.73 -    finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
    3.74 +    finally show "x \<cdot> y \<^loc>\<le> z" by(simp add:below_def)
    3.75    next
    3.76 -    assume a: "y \<sqsubseteq> z"
    3.77 +    assume a: "y \<^loc>\<le> z"
    3.78      have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
    3.79      also have "y \<cdot> z = y" using a by(simp add:below_def)
    3.80 -    finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
    3.81 +    finally show "x \<cdot> y \<^loc>\<le> z" by(simp add:below_def)
    3.82    qed
    3.83  qed
    3.84  
    3.85 -lemma strict_below_f_conv[simp,noatp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
    3.86 +lemma strict_below_f_conv[simp,noatp]: "x \<^loc>< y \<cdot> z = (x \<^loc>< y \<and> x \<^loc>< z)"
    3.87  apply(simp add: strict_below_def)
    3.88  using lin[of y z] by (auto simp:below_def ACI)
    3.89  
    3.90  lemma strict_above_f_conv:
    3.91 -  "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)"
    3.92 +  "x \<cdot> y \<^loc>< z = (x \<^loc>< z \<or> y \<^loc>< z)"
    3.93  apply(simp add: strict_below_def above_f_conv)
    3.94  using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
    3.95  
    3.96 @@ -2150,18 +2150,18 @@
    3.97  
    3.98  lemma (in ACIfSL) below_fold1_iff:
    3.99  assumes A: "finite A" "A \<noteq> {}"
   3.100 -shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
   3.101 +shows "x \<^loc>\<le> fold1 f A = (\<forall>a\<in>A. x \<^loc>\<le> a)"
   3.102  using A
   3.103  by(induct rule:finite_ne_induct) simp_all
   3.104  
   3.105  lemma (in ACIfSLlin) strict_below_fold1_iff:
   3.106 -  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<sqsubset> fold1 f A = (\<forall>a\<in>A. x \<sqsubset> a)"
   3.107 +  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<^loc>< fold1 f A = (\<forall>a\<in>A. x \<^loc>< a)"
   3.108  by(induct rule:finite_ne_induct) simp_all
   3.109  
   3.110  
   3.111  lemma (in ACIfSL) fold1_belowI:
   3.112  assumes A: "finite A" "A \<noteq> {}"
   3.113 -shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
   3.114 +shows "a \<in> A \<Longrightarrow> fold1 f A \<^loc>\<le> a"
   3.115  using A
   3.116  proof (induct rule:finite_ne_induct)
   3.117    case singleton thus ?case by simp
   3.118 @@ -2173,7 +2173,7 @@
   3.119      assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
   3.120    next
   3.121      assume "a \<in> F"
   3.122 -    hence bel: "fold1 f F \<sqsubseteq> a" by(rule insert)
   3.123 +    hence bel: "fold1 f F \<^loc>\<le> a" by(rule insert)
   3.124      have "fold1 f (insert x F) \<cdot> a = x \<cdot> (fold1 f F \<cdot> a)"
   3.125        using insert by(simp add:below_def ACI)
   3.126      also have "fold1 f F \<cdot> a = fold1 f F"
   3.127 @@ -2186,19 +2186,19 @@
   3.128  
   3.129  lemma (in ACIfSLlin) fold1_below_iff:
   3.130  assumes A: "finite A" "A \<noteq> {}"
   3.131 -shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
   3.132 +shows "fold1 f A \<^loc>\<le> x = (\<exists>a\<in>A. a \<^loc>\<le> x)"
   3.133  using A
   3.134  by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
   3.135  
   3.136  lemma (in ACIfSLlin) fold1_strict_below_iff:
   3.137  assumes A: "finite A" "A \<noteq> {}"
   3.138 -shows "fold1 f A \<sqsubset> x = (\<exists>a\<in>A. a \<sqsubset> x)"
   3.139 +shows "fold1 f A \<^loc>< x = (\<exists>a\<in>A. a \<^loc>< x)"
   3.140  using A
   3.141  by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
   3.142  
   3.143  lemma (in ACIfSLlin) fold1_antimono:
   3.144  assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
   3.145 -shows "fold1 f B \<sqsubseteq> fold1 f A"
   3.146 +shows "fold1 f B \<^loc>\<le> fold1 f A"
   3.147  proof(cases)
   3.148    assume "A = B" thus ?thesis by simp
   3.149  next
   3.150 @@ -2213,7 +2213,7 @@
   3.151      moreover have "A Int (B-A) = {}" using prems by blast
   3.152      ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
   3.153    qed
   3.154 -  also have "\<dots> \<sqsubseteq> fold1 f A" by(simp add: above_f_conv)
   3.155 +  also have "\<dots> \<^loc>\<le> fold1 f A" by(simp add: above_f_conv)
   3.156    finally show ?thesis .
   3.157  qed
   3.158  
   3.159 @@ -2285,7 +2285,7 @@
   3.160  where
   3.161    "Sup_fin = fold1 (op \<squnion>)"
   3.162  
   3.163 -lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<sqsubseteq> \<Squnion>\<^bsub>fin\<^esub>A"
   3.164 +lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<^loc>\<le> \<Squnion>\<^bsub>fin\<^esub>A"
   3.165  apply(unfold Sup_fin_def Inf_fin_def)
   3.166  apply(subgoal_tac "EX a. a:A")
   3.167  prefer 2 apply blast
     4.1 --- a/src/HOL/HOL.thy	Fri Sep 28 10:35:53 2007 +0200
     4.2 +++ b/src/HOL/HOL.thy	Sat Sep 29 08:58:51 2007 +0200
     4.3 @@ -244,8 +244,8 @@
     4.4    abs  ("\<bar>_\<bar>")
     4.5  
     4.6  class ord = type +
     4.7 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
     4.8 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
     4.9 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    4.10 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    4.11  begin
    4.12  
    4.13  notation
     5.1 --- a/src/HOL/Library/Kleene_Algebras.thy	Fri Sep 28 10:35:53 2007 +0200
     5.2 +++ b/src/HOL/Library/Kleene_Algebras.thy	Sat Sep 29 08:58:51 2007 +0200
     5.3 @@ -22,8 +22,8 @@
     5.4    by simp
     5.5  
     5.6  class order_by_add = idem_add + ord +
     5.7 -  assumes order_def: "a \<sqsubseteq> b \<longleftrightarrow> a \<^loc>+ b = b"
     5.8 -  assumes strict_order_def: "a \<sqsubset> b \<longleftrightarrow> a \<sqsubseteq> b \<and> a \<noteq> b"
     5.9 +  assumes order_def: "a \<^loc>\<le> b \<longleftrightarrow> a \<^loc>+ b = b"
    5.10 +  assumes strict_order_def: "a \<^loc>< b \<longleftrightarrow> a \<^loc>\<le> b \<and> a \<noteq> b"
    5.11  
    5.12  lemma ord_simp1[simp]: "(x::'a::order_by_add) \<le> y \<Longrightarrow> x + y = y"
    5.13    unfolding order_def .
    5.14 @@ -82,14 +82,14 @@
    5.15  qed
    5.16  
    5.17  class kleene = pre_kleene + star +
    5.18 -  assumes star1: "\<^loc>1 \<^loc>+ a \<^loc>* star a \<sqsubseteq> star a"
    5.19 -  and star2: "\<^loc>1 \<^loc>+ star a \<^loc>* a \<sqsubseteq> star a"
    5.20 -  and star3: "a \<^loc>* x \<sqsubseteq> x \<Longrightarrow> star a \<^loc>* x \<sqsubseteq> x"
    5.21 -  and star4: "x \<^loc>* a \<sqsubseteq> x \<Longrightarrow> x \<^loc>* star a \<sqsubseteq> x"
    5.22 +  assumes star1: "\<^loc>1 \<^loc>+ a \<^loc>* star a \<^loc>\<le> star a"
    5.23 +  and star2: "\<^loc>1 \<^loc>+ star a \<^loc>* a \<^loc>\<le> star a"
    5.24 +  and star3: "a \<^loc>* x \<^loc>\<le> x \<Longrightarrow> star a \<^loc>* x \<^loc>\<le> x"
    5.25 +  and star4: "x \<^loc>* a \<^loc>\<le> x \<Longrightarrow> x \<^loc>* star a \<^loc>\<le> x"
    5.26  
    5.27 -class kleene_by_complete_lattice =
    5.28 -  pre_kleene + complete_lattice + recpower + star +
    5.29 -  assumes star_cont: "a \<^loc>* star b \<^loc>* c = (SUP n. a \<^loc>* b ^ n \<^loc>* c)"
    5.30 +class kleene_by_complete_lattice = pre_kleene
    5.31 +  + complete_lattice + recpower + star +
    5.32 +  assumes star_cont: "a \<^loc>* star b \<^loc>* c = SUPR UNIV (\<lambda>n. a \<^loc>* b \<^loc>^ n \<^loc>* c)"
    5.33  
    5.34  lemma plus_leI: 
    5.35    fixes x :: "'a :: order_by_add"
     6.1 --- a/src/HOL/List.thy	Fri Sep 28 10:35:53 2007 +0200
     6.2 +++ b/src/HOL/List.thy	Sat Sep 29 08:58:51 2007 +0200
     6.3 @@ -2542,9 +2542,9 @@
     6.4  
     6.5  class finite_intvl_succ = linorder +
     6.6  fixes successor :: "'a \<Rightarrow> 'a"
     6.7 -assumes finite_intvl: "finite(ord.atLeastAtMost (op \<sqsubseteq>) a b)" (* FIXME should be finite({a..b}) *)
     6.8 -and successor_incr: "a \<sqsubset> successor a"
     6.9 -and ord_discrete: "\<not>(\<exists>x. a \<sqsubset> x & x \<sqsubset> successor a)"
    6.10 +assumes finite_intvl: "finite(ord.atLeastAtMost (op \<^loc>\<le>) a b)" (* FIXME should be finite({a..b}) *)
    6.11 +and successor_incr: "a \<^loc>< successor a"
    6.12 +and ord_discrete: "\<not>(\<exists>x. a \<^loc>< x & x \<^loc>< successor a)"
    6.13  
    6.14  context finite_intvl_succ
    6.15  begin
    6.16 @@ -2565,9 +2565,9 @@
    6.17  apply (metis ord_discrete less_le not_le)
    6.18  done
    6.19  
    6.20 -lemma upto_rec[code]: "\<^loc>[i..j] = (if i \<sqsubseteq> j then i # \<^loc>[successor i..j] else [])"
    6.21 +lemma upto_rec[code]: "\<^loc>[i..j] = (if i \<^loc>\<le> j then i # \<^loc>[successor i..j] else [])"
    6.22  proof cases
    6.23 -  assume "i \<sqsubseteq> j" thus ?thesis
    6.24 +  assume "i \<^loc>\<le> j" thus ?thesis
    6.25      apply(simp add:upto_def)
    6.26      apply (rule the1_equality[OF finite_sorted_distinct_unique])
    6.27       apply (simp add:finite_intvl)
    6.28 @@ -2577,7 +2577,7 @@
    6.29      apply (metis successor_incr leD less_imp_le order_trans)
    6.30      done
    6.31  next
    6.32 -  assume "~ i \<sqsubseteq> j" thus ?thesis
    6.33 +  assume "~ i \<^loc>\<le> j" thus ?thesis
    6.34      by(simp add:upto_def atLeastAtMost_empty cong:conj_cong)
    6.35  qed
    6.36  
     7.1 --- a/src/HOL/OrderedGroup.thy	Fri Sep 28 10:35:53 2007 +0200
     7.2 +++ b/src/HOL/OrderedGroup.thy	Sat Sep 29 08:58:51 2007 +0200
     7.3 @@ -216,13 +216,13 @@
     7.4  subsection {* (Partially) Ordered Groups *} 
     7.5  
     7.6  class pordered_ab_semigroup_add = order + ab_semigroup_add +
     7.7 -  assumes add_left_mono: "a \<sqsubseteq> b \<Longrightarrow> c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b"
     7.8 +  assumes add_left_mono: "a \<^loc>\<le> b \<Longrightarrow> c \<^loc>+ a \<^loc>\<le> c \<^loc>+ b"
     7.9  
    7.10  class pordered_cancel_ab_semigroup_add =
    7.11    pordered_ab_semigroup_add + cancel_ab_semigroup_add
    7.12  
    7.13  class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
    7.14 -  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b"
    7.15 +  assumes add_le_imp_le_left: "c \<^loc>+ a \<^loc>\<le> c \<^loc>+ b \<Longrightarrow> a \<^loc>\<le> b"
    7.16  
    7.17  class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
    7.18  
     8.1 --- a/src/HOL/Orderings.thy	Fri Sep 28 10:35:53 2007 +0200
     8.2 +++ b/src/HOL/Orderings.thy	Sat Sep 29 08:58:51 2007 +0200
     8.3 @@ -14,13 +14,18 @@
     8.4  subsection {* Partial orders *}
     8.5  
     8.6  class order = ord +
     8.7 -  assumes less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
     8.8 -  and order_refl [iff]: "x \<sqsubseteq> x"
     8.9 -  and order_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
    8.10 -  assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
    8.11 +  assumes less_le: "x \<^loc>< y \<longleftrightarrow> x \<^loc>\<le> y \<and> x \<noteq> y"
    8.12 +  and order_refl [iff]: "x \<^loc>\<le> x"
    8.13 +  and order_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> z"
    8.14 +  assumes antisym: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
    8.15  
    8.16  begin
    8.17  
    8.18 +notation (input)
    8.19 +  less_eq (infix "\<sqsubseteq>" 50)
    8.20 +and
    8.21 +  less    (infix "\<sqsubset>" 50)
    8.22 +
    8.23  text {* Reflexivity. *}
    8.24  
    8.25  lemma eq_refl: "x = y \<Longrightarrow> x \<^loc>\<le> y"
     9.1 --- a/src/HOL/Real/RealVector.thy	Fri Sep 28 10:35:53 2007 +0200
     9.2 +++ b/src/HOL/Real/RealVector.thy	Sat Sep 29 08:58:51 2007 +0200
     9.3 @@ -44,13 +44,19 @@
     9.4  subsection {* Real vector spaces *}
     9.5  
     9.6  class scaleR = type +
     9.7 -  fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a"
     9.8 -
     9.9 -notation
    9.10 -  scaleR (infixr "*#" 75)
    9.11 +  fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<^loc>*#" 75)
    9.12 +begin
    9.13  
    9.14  abbreviation
    9.15 -  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a::scaleR" (infixl "'/#" 70) where
    9.16 +  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "\<^loc>'/#" 70)
    9.17 +where
    9.18 +  "x \<^loc>/# r == scaleR (inverse r) x"
    9.19 +
    9.20 +end
    9.21 +
    9.22 +abbreviation
    9.23 +  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a\<Colon>scaleR" (infixl "'/#" 70)
    9.24 +where
    9.25    "x /# r == scaleR (inverse r) x"
    9.26  
    9.27  notation (xsymbols)
    9.28 @@ -378,7 +384,7 @@
    9.29    real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
    9.30  
    9.31  class sgn_div_norm = scaleR + norm + sgn +
    9.32 -  assumes sgn_div_norm: "sgn x = x /# norm x"
    9.33 +  assumes sgn_div_norm: "sgn x = x \<^loc>/# norm x"
    9.34  
    9.35  class real_normed_vector = real_vector + sgn_div_norm +
    9.36    assumes norm_ge_zero [simp]: "0 \<le> norm x"
    10.1 --- a/src/HOL/Ring_and_Field.thy	Fri Sep 28 10:35:53 2007 +0200
    10.2 +++ b/src/HOL/Ring_and_Field.thy	Sat Sep 29 08:58:51 2007 +0200
    10.3 @@ -153,7 +153,7 @@
    10.4  qed
    10.5  
    10.6  class field = comm_ring_1 + inverse +
    10.7 -  assumes field_inverse:  "a \<noteq> 0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
    10.8 +  assumes field_inverse:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
    10.9    assumes divide_inverse: "a \<^loc>/ b = a \<^loc>* inverse b"
   10.10  
   10.11  instance field \<subseteq> division_ring
   10.12 @@ -211,8 +211,8 @@
   10.13  lemmas ring_simps = group_simps ring_distribs
   10.14  
   10.15  class mult_mono = times + zero + ord +
   10.16 -  assumes mult_left_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
   10.17 -  assumes mult_right_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> a \<^loc>* c \<sqsubseteq> b \<^loc>* c"
   10.18 +  assumes mult_left_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"
   10.19 +  assumes mult_right_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> a \<^loc>* c \<^loc>\<le> b \<^loc>* c"
   10.20  
   10.21  class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
   10.22  
   10.23 @@ -228,8 +228,8 @@
   10.24  instance ordered_semiring \<subseteq> pordered_cancel_semiring ..
   10.25  
   10.26  class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
   10.27 -  assumes mult_strict_left_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
   10.28 -  assumes mult_strict_right_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> a \<^loc>* c \<sqsubset> b \<^loc>* c"
   10.29 +  assumes mult_strict_left_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"
   10.30 +  assumes mult_strict_right_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> a \<^loc>* c \<^loc>< b \<^loc>* c"
   10.31  
   10.32  instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
   10.33  
   10.34 @@ -246,7 +246,7 @@
   10.35  qed
   10.36  
   10.37  class mult_mono1 = times + zero + ord +
   10.38 -  assumes mult_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
   10.39 +  assumes mult_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"
   10.40  
   10.41  class pordered_comm_semiring = comm_semiring_0
   10.42    + pordered_ab_semigroup_add + mult_mono1
   10.43 @@ -257,7 +257,7 @@
   10.44  instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
   10.45  
   10.46  class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
   10.47 -  assumes mult_strict_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
   10.48 +  assumes mult_strict_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"
   10.49  
   10.50  instance pordered_comm_semiring \<subseteq> pordered_semiring
   10.51  proof
   10.52 @@ -297,10 +297,10 @@
   10.53  instance lordered_ring \<subseteq> lordered_ab_group_join ..
   10.54  
   10.55  class abs_if = minus + ord + zero + abs +
   10.56 -  assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
   10.57 +  assumes abs_if: "abs a = (if a \<^loc>< \<^loc>0 then (uminus a) else a)"
   10.58  
   10.59  class sgn_if = sgn + zero + one + minus + ord +
   10.60 -assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 \<sqsubset> x then 1 else uminus 1)"
   10.61 +  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)"
   10.62  
   10.63  (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
   10.64     Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.
   10.65 @@ -327,7 +327,7 @@
   10.66  
   10.67  class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
   10.68    (*previously ordered_semiring*)
   10.69 -  assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
   10.70 +  assumes zero_less_one [simp]: "\<^loc>0 \<^loc>< \<^loc>1"
   10.71  
   10.72  lemma pos_add_strict:
   10.73    fixes a b c :: "'a\<Colon>ordered_semidom"
    11.1 --- a/src/HOL/SetInterval.thy	Fri Sep 28 10:35:53 2007 +0200
    11.2 +++ b/src/HOL/SetInterval.thy	Sat Sep 29 08:58:51 2007 +0200
    11.3 @@ -17,19 +17,19 @@
    11.4  begin
    11.5  definition
    11.6    lessThan    :: "'a => 'a set"	("(1\<^loc>{..<_})") where
    11.7 -  "\<^loc>{..<u} == {x. x \<sqsubset> u}"
    11.8 +  "\<^loc>{..<u} == {x. x \<^loc>< u}"
    11.9  
   11.10  definition
   11.11    atMost      :: "'a => 'a set"	("(1\<^loc>{.._})") where
   11.12 -  "\<^loc>{..u} == {x. x \<sqsubseteq> u}"
   11.13 +  "\<^loc>{..u} == {x. x \<^loc>\<le> u}"
   11.14  
   11.15  definition
   11.16    greaterThan :: "'a => 'a set"	("(1\<^loc>{_<..})") where
   11.17 -  "\<^loc>{l<..} == {x. l\<sqsubset>x}"
   11.18 +  "\<^loc>{l<..} == {x. l\<^loc><x}"
   11.19  
   11.20  definition
   11.21    atLeast     :: "'a => 'a set"	("(1\<^loc>{_..})") where
   11.22 -  "\<^loc>{l..} == {x. l\<sqsubseteq>x}"
   11.23 +  "\<^loc>{l..} == {x. l\<^loc>\<le>x}"
   11.24  
   11.25  definition
   11.26    greaterThanLessThan :: "'a => 'a => 'a set"  ("(1\<^loc>{_<..<_})") where
    12.1 --- a/src/Pure/Isar/class.ML	Fri Sep 28 10:35:53 2007 +0200
    12.2 +++ b/src/Pure/Isar/class.ML	Sat Sep 29 08:58:51 2007 +0200
    12.3 @@ -13,9 +13,9 @@
    12.4      -> ((bstring * Attrib.src list) * string list) list
    12.5      -> theory -> class * theory
    12.6    val classrel_cmd: xstring * xstring -> theory -> Proof.state
    12.7 -  val class: bstring -> class list -> Element.context_i Locale.element list
    12.8 +  val class: bool -> bstring -> class list -> Element.context_i Locale.element list
    12.9      -> string list -> theory -> string * Proof.context
   12.10 -  val class_cmd: bstring -> xstring list -> Element.context Locale.element list
   12.11 +  val class_cmd: bool -> bstring -> xstring list -> Element.context Locale.element list
   12.12      -> xstring list -> theory -> string * Proof.context
   12.13    val add_const_in_class: string -> (string * term) * Syntax.mixfix
   12.14      -> theory -> theory
   12.15 @@ -25,6 +25,7 @@
   12.16    val intro_classes_tac: thm list -> tactic
   12.17    val default_intro_classes_tac: thm list -> tactic
   12.18    val class_of_locale: theory -> string -> class option
   12.19 +  val local_syntax: theory -> class -> bool
   12.20    val print_classes: theory -> unit
   12.21  
   12.22    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
   12.23 @@ -46,12 +47,12 @@
   12.24    val params_of_sort: theory -> sort -> (string * (string * typ)) list
   12.25  
   12.26    (*experimental*)
   12.27 -  val init_ref: (class -> Proof.context -> (theory -> theory) * Proof.context) ref
   12.28 -  val init: class -> Proof.context -> (theory -> theory) * Proof.context;
   12.29 -  val init_default: class -> Proof.context -> (theory -> theory) * Proof.context;
   12.30 -  val remove_constraints: class -> theory -> (string * typ) list * theory
   12.31 -  val class_term_check: theory -> class -> term list -> Proof.context -> term list * Proof.context
   12.32 -  val local_param: theory -> class -> string -> (term * (class * int)) option
   12.33 +  val init_ref: (sort -> Proof.context -> Proof.context) ref
   12.34 +  val init: sort -> Proof.context -> Proof.context;
   12.35 +  val init_default: sort -> Proof.context -> Proof.context;
   12.36 +  val local_param: theory -> sort -> string -> (term * (class * int)) option
   12.37 +  val remove_constraints': sort -> theory -> (string * typ) list * theory
   12.38 +  val remove_constraints: sort -> Proof.context -> (string * typ) list * Proof.context
   12.39  end;
   12.40  
   12.41  structure Class : CLASS =
   12.42 @@ -99,7 +100,7 @@
   12.43        | NONE => thm;
   12.44    in strip end;
   12.45  
   12.46 -fun get_remove_contraint c thy =
   12.47 +fun get_remove_constraint c thy =
   12.48    let
   12.49      val ty = Sign.the_const_constraint thy c;
   12.50    in
   12.51 @@ -298,7 +299,7 @@
   12.52        #> after_qed defs;
   12.53    in
   12.54      theory
   12.55 -    |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
   12.56 +    |> fold_map get_remove_constraint (map fst cs |> distinct (op =))
   12.57      ||>> fold_map add_def defs
   12.58      ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
   12.59      |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
   12.60 @@ -329,26 +330,27 @@
   12.61    locale: string,
   12.62    consts: (string * string) list
   12.63      (*locale parameter ~> theory constant name*),
   12.64 -  v: string,
   12.65 +  local_sort: sort,
   12.66    inst: typ Symtab.table * term Symtab.table
   12.67      (*canonical interpretation*),
   12.68    intro: thm,
   12.69 +  local_syntax: bool,
   12.70    defs: thm list,
   12.71    localized: (string * (term * (class * int))) list
   12.72      (*theory constant name ~> (locale parameter, (class, instantiaton index of class typ))*)
   12.73  };
   12.74  
   12.75  fun rep_class_data (ClassData d) = d;
   12.76 -fun mk_class_data ((locale, consts, v, inst, intro), (defs, localized)) =
   12.77 -  ClassData { locale = locale, consts = consts, v = v, inst = inst, intro = intro,
   12.78 -    defs = defs, localized = localized };
   12.79 -fun map_class_data f (ClassData { locale, consts, v, inst, intro, defs, localized }) =
   12.80 -  mk_class_data (f ((locale, consts, v, inst, intro), (defs, localized)))
   12.81 -fun merge_class_data _ (ClassData { locale = locale, consts = consts, v = v, inst = inst,
   12.82 -    intro = intro, defs = defs1, localized = localized1 },
   12.83 -  ClassData { locale = _, consts = _, v = _, inst = _, intro = _,
   12.84 +fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)) =
   12.85 +  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro,
   12.86 +    local_syntax = local_syntax, defs = defs, localized = localized };
   12.87 +fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, localized }) =
   12.88 +  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)))
   12.89 +fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
   12.90 +    intro = intro, local_syntax = local_syntax, defs = defs1, localized = localized1 },
   12.91 +  ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _,
   12.92      defs = defs2, localized = localized2 }) =
   12.93 -  mk_class_data ((locale, consts, v, inst, intro),
   12.94 +  mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
   12.95      (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (localized1, localized2)));
   12.96  
   12.97  fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
   12.98 @@ -393,11 +395,13 @@
   12.99    Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
  12.100      ((fst o ClassData.get) thy) [];
  12.101  
  12.102 -fun these_localized thy class =
  12.103 -  maps (#localized o the_class_data thy) (ancestry thy [class]);
  12.104 +fun these_localized thy =
  12.105 +  maps (#localized o the_class_data thy) o ancestry thy;
  12.106  
  12.107  fun local_param thy = AList.lookup (op =) o these_localized thy;
  12.108  
  12.109 +fun local_syntax thy = #local_syntax o the_class_data thy
  12.110 +
  12.111  fun print_classes thy =
  12.112    let
  12.113      val algebra = Sign.classes_of thy;
  12.114 @@ -433,11 +437,11 @@
  12.115  
  12.116  (* updaters *)
  12.117  
  12.118 -fun add_class_data ((class, superclasses), (locale, consts, v, inst, intro)) =
  12.119 +fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) =
  12.120    ClassData.map (fn (gr, tab) => (
  12.121      gr
  12.122 -    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, v, inst, intro),
  12.123 -         ([], map (apsnd (rpair (class, 0) o Free) o swap) consts)))
  12.124 +    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst,
  12.125 +         intro, local_syntax), ([], map (apsnd (rpair (class, 0) o Free) o swap) consts)))
  12.126      |> fold (curry Graph.add_edge class) superclasses,
  12.127      tab
  12.128      |> Symtab.update (locale, class)
  12.129 @@ -539,6 +543,90 @@
  12.130  
  12.131  (** classes and class target **)
  12.132  
  12.133 +(* class context initialization *)
  12.134 +
  12.135 +(*experimental*)
  12.136 +fun get_remove_constraint_ctxt c ctxt =
  12.137 +  let
  12.138 +    val ty = ProofContext.the_const_constraint ctxt c;
  12.139 +  in
  12.140 +    ctxt
  12.141 +    |> ProofContext.add_const_constraint (c, NONE)
  12.142 +    |> pair (c, ty)
  12.143 +  end;
  12.144 +
  12.145 +fun remove_constraints' class thy =
  12.146 +  thy |> fold_map (get_remove_constraint o fst) (these_localized thy class);
  12.147 +
  12.148 +fun remove_constraints class ctxt =
  12.149 +  ctxt |> fold_map (get_remove_constraint_ctxt o fst) (these_localized (ProofContext.theory_of ctxt) class);
  12.150 +
  12.151 +fun default_typ ctxt constraints c =
  12.152 +  case AList.lookup (op =) constraints c
  12.153 +   of SOME ty => SOME ty
  12.154 +    | NONE => try (Consts.the_constraint (ProofContext.consts_of ctxt)) c;
  12.155 +
  12.156 +fun infer_constraints ctxt constraints ts =
  12.157 +    TypeInfer.infer_types (ProofContext.pp ctxt) (Sign.tsig_of (ProofContext.theory_of ctxt))
  12.158 +     (Syntax.check_typs ctxt)
  12.159 +      (default_typ ctxt constraints) (K NONE)
  12.160 +      (Variable.names_of ctxt) true (map (rpair dummyT) ts)
  12.161 +    |> #1 |> map #1
  12.162 +  handle TYPE (msg, _, _) => error msg
  12.163 +
  12.164 +fun subst_typ local_sort =
  12.165 +  map_atyps (fn (t as TFree (v, _)) => if v = AxClass.param_tyvarname
  12.166 +        then TFree (v, local_sort)
  12.167 +        else t
  12.168 +    | t => t);
  12.169 +
  12.170 +fun sort_typ_check thy sort =
  12.171 +  let
  12.172 +    val local_sort = (#local_sort o the_class_data thy) (hd sort);
  12.173 +  in
  12.174 +    pair o map (subst_typ local_sort)
  12.175 +  end;
  12.176 +
  12.177 +fun sort_term_check thy sort constraints =
  12.178 +  let
  12.179 +    val algebra = Sign.classes_of thy;
  12.180 +    val local_sort = (#local_sort o the_class_data thy) (hd sort);
  12.181 +    val v = AxClass.param_tyvarname;
  12.182 +    val local_param = local_param thy sort;
  12.183 +      (*FIXME efficiency*)
  12.184 +    fun class_arg c idx ty =
  12.185 +      let
  12.186 +        val typargs = Sign.const_typargs thy (c, ty);
  12.187 +        fun classtyp (TFree (w, _)) = w = v
  12.188 +          | classtyp t = false;
  12.189 +      in classtyp (nth typargs idx) end;
  12.190 +    fun subst (t as Const (c, ty)) = (case local_param c
  12.191 +         of NONE => t
  12.192 +          | SOME (t', (_, idx)) => if class_arg c idx ty
  12.193 +             then t' else t)
  12.194 +      | subst t = t;
  12.195 +  in fn ts => fn ctxt =>
  12.196 +    ((map (map_aterms subst) #> infer_constraints ctxt constraints) ts, ctxt)
  12.197 +  end;
  12.198 +
  12.199 +fun init_default sort ctxt =
  12.200 +  let
  12.201 +    val thy = ProofContext.theory_of ctxt;
  12.202 +    val typ_check = sort_typ_check thy sort;
  12.203 +    val term_check = sort_term_check thy sort;
  12.204 +  in
  12.205 +    ctxt
  12.206 +    |> remove_constraints sort
  12.207 +    ||> Variable.declare_term (Logic.mk_type (TFree (AxClass.param_tyvarname, sort)))
  12.208 +    ||> Context.proof_map (Syntax.add_typ_check typ_check)
  12.209 +    |-> (fn constraints =>
  12.210 +        Context.proof_map (Syntax.add_term_check (term_check constraints)))
  12.211 +  end;
  12.212 +
  12.213 +val init_ref = ref (K I : sort -> Proof.context -> Proof.context);
  12.214 +fun init class = ! init_ref class;
  12.215 +
  12.216 +
  12.217  (* class definition *)
  12.218  
  12.219  local
  12.220 @@ -551,52 +639,62 @@
  12.221      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
  12.222    end;
  12.223  
  12.224 -fun gen_class add_locale prep_class prep_param bname
  12.225 -    raw_supclasses raw_elems raw_other_consts thy =
  12.226 +fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
  12.227    let
  12.228 +    val supclasses = map (prep_class thy) raw_supclasses;
  12.229 +    val sups = filter (is_some o lookup_class_data thy) supclasses
  12.230 +      |> Sign.minimize_sort thy;
  12.231 +    val supsort = Sign.minimize_sort thy supclasses;
  12.232 +    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
  12.233 +    val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
  12.234 +      | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
  12.235 +    val supexpr = Locale.Merge suplocales;
  12.236 +    val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
  12.237 +    val supconsts = AList.make (the o AList.lookup (op =) (params_of_sort thy sups))
  12.238 +      (map fst supparams);
  12.239 +    val mergeexpr = Locale.Merge (suplocales @ includes);
  12.240 +    val constrain = Element.Constrains ((map o apsnd o map_atyps)
  12.241 +      (fn TFree (_, sort) => TFree (AxClass.param_tyvarname, sort)) supparams);
  12.242 +  in
  12.243 +    ProofContext.init thy
  12.244 +    |> Locale.cert_expr supexpr [constrain]
  12.245 +    |> snd
  12.246 +    |> init supsort
  12.247 +    |> process_expr Locale.empty raw_elems
  12.248 +    |> fst
  12.249 +    |> (fn elems => ((((sups, supconsts), (supsort, mergeexpr)),
  12.250 +          (*FIXME*) if null includes then constrain :: elems else elems)))
  12.251 +  end;
  12.252 +
  12.253 +val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
  12.254 +val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
  12.255 +
  12.256 +fun gen_class prep_spec prep_param local_syntax bname
  12.257 +    raw_supclasses raw_includes_elems raw_other_consts thy =
  12.258 +  let
  12.259 +    val (((sups, supconsts), (supsort, mergeexpr)), elems) =
  12.260 +      prep_spec thy raw_supclasses raw_includes_elems;
  12.261 +    val other_consts = map (prep_param thy) raw_other_consts;
  12.262      fun mk_instT class = Symtab.empty
  12.263        |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
  12.264      fun mk_inst class param_names cs =
  12.265        Symtab.empty
  12.266        |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
  12.267             (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
  12.268 -    (*FIXME need proper concept for reading locale statements*)
  12.269 -    fun subst_classtyvar (_, _) =
  12.270 -          TFree (AxClass.param_tyvarname, [])
  12.271 -      | subst_classtyvar (v, sort) =
  12.272 -          error ("Sort constraint illegal in type class, for type variable "
  12.273 -            ^ v ^ "::" ^ Sign.string_of_sort thy sort);
  12.274 -    (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
  12.275 -      typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
  12.276 -    val other_consts = map (prep_param thy) raw_other_consts;
  12.277 -    val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
  12.278 -      | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
  12.279 -    val supclasses = map (prep_class thy) raw_supclasses;
  12.280 -    val sups = filter (is_some o lookup_class_data thy) supclasses
  12.281 -      |> Sign.minimize_sort thy;
  12.282 -    val supsort = Sign.minimize_sort thy supclasses;
  12.283 -    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
  12.284 -    val supexpr = Locale.Merge (suplocales @ includes);
  12.285 -    val supparams = (map fst o Locale.parameters_of_expr thy)
  12.286 -      (Locale.Merge suplocales);
  12.287 -    val supconsts = AList.make (the o AList.lookup (op =) (params_of_sort thy sups))
  12.288 -      (map fst supparams);
  12.289 -    (*val elems_constrains = map
  12.290 -      (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
  12.291 -    fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname,
  12.292 -      if Sign.subsort thy (supsort, sort) then sort else error
  12.293 -        ("Sort " ^ Sign.string_of_sort thy sort
  12.294 -          ^ " is less general than permitted least general sort "
  12.295 -          ^ Sign.string_of_sort thy supsort));
  12.296      fun extract_params thy name_locale =
  12.297        let
  12.298          val params = Locale.parameters_of thy name_locale;
  12.299 -        val v = case (maps typ_tfrees o map (snd o fst)) params
  12.300 -         of (v, _) :: _ => v
  12.301 -          | [] => AxClass.param_tyvarname;
  12.302 +        val local_sort = case AList.group (op =) ((maps typ_tfrees o map (snd o fst)) params)
  12.303 +         of [(_, local_sort :: _)] => local_sort
  12.304 +          | _ => Sign.defaultS thy
  12.305 +          | vs => error ("exactly one type variable required: " ^ commas (map fst vs));
  12.306 +        val _ = if Sign.subsort thy (supsort, local_sort) then () else error
  12.307 +          ("Sort " ^ Sign.string_of_sort thy local_sort
  12.308 +            ^ " is less general than permitted least general sort "
  12.309 +            ^ Sign.string_of_sort thy supsort);
  12.310        in
  12.311 -        (v, (map fst params, params
  12.312 -        |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
  12.313 +        (local_sort, (map fst params, params
  12.314 +        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, local_sort)))
  12.315          |> (map o apsnd) (fork_mixfix true NONE #> fst)
  12.316          |> chop (length supconsts)
  12.317          |> snd))
  12.318 @@ -620,19 +718,19 @@
  12.319        #> snd
  12.320    in
  12.321      thy
  12.322 -    |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
  12.323 +    |> Locale.add_locale_i (SOME "") bname mergeexpr elems
  12.324      |-> (fn name_locale => ProofContext.theory_result (
  12.325        `(fn thy => extract_params thy name_locale)
  12.326 -      #-> (fn (v, (globals, params)) =>
  12.327 +      #-> (fn (local_sort, (globals, params)) =>
  12.328          AxClass.define_class_params (bname, supsort) params
  12.329            (extract_assumes name_locale params) other_consts
  12.330        #-> (fn (name_axclass, (consts, axioms)) =>
  12.331          `(fn thy => class_intro thy name_locale name_axclass sups)
  12.332        #-> (fn class_intro =>
  12.333          add_class_data ((name_axclass, sups),
  12.334 -          (name_locale, map fst params ~~ map fst consts, v,
  12.335 +          (name_locale, map fst params ~~ map fst consts, local_sort,
  12.336              (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
  12.337 -              (map snd supconsts @ consts)), class_intro))
  12.338 +              (map snd supconsts @ consts)), class_intro, local_syntax))
  12.339        #> note_intro name_axclass class_intro
  12.340        #> class_interpretation name_axclass axioms []
  12.341        #> pair name_axclass
  12.342 @@ -641,18 +739,12 @@
  12.343  
  12.344  in
  12.345  
  12.346 -val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param;
  12.347 -val class = gen_class Locale.add_locale_i Sign.certify_class (K I);
  12.348 +val class_cmd = gen_class read_class_spec read_param;
  12.349 +val class = gen_class check_class_spec (K I);
  12.350  
  12.351  end; (*local*)
  12.352  
  12.353  
  12.354 -(* class target context *)
  12.355 -
  12.356 -fun remove_constraints class thy =
  12.357 -  thy |> fold_map (get_remove_contraint o fst) (these_localized thy class);
  12.358 -
  12.359 -
  12.360  (* definition in class target *)
  12.361  
  12.362  fun export_fixes thy class =
  12.363 @@ -673,11 +765,10 @@
  12.364          val n2 = NameSpace.qualifier n1;
  12.365          val n3 = NameSpace.base n1;
  12.366        in NameSpace.implode [n2, prfx, n3] end;
  12.367 -    val v = (#v o the_class_data thy) class;
  12.368      val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
  12.369 +    val rhs' = export_fixes thy class rhs;
  12.370      val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
  12.371 -      if w = v then TFree (w, constrain_sort sort) else TFree var);
  12.372 -    val rhs' = export_fixes thy class rhs;
  12.373 +      if w = AxClass.param_tyvarname then TFree (w, constrain_sort sort) else TFree var);
  12.374      val ty' = Term.fastype_of rhs';
  12.375      val ty'' = subst_typ ty';
  12.376      val c' = mk_name c;
  12.377 @@ -688,7 +779,7 @@
  12.378          val def' = symmetric def;
  12.379          val def_eq = Thm.prop_of def';
  12.380          val typargs = Sign.const_typargs thy (c', fastype_of rhs);
  12.381 -        val typidx = find_index (fn TFree (w, _) => v = w | _ => false) typargs;
  12.382 +        val typidx = find_index (fn TFree (w, _) => AxClass.param_tyvarname = w | _ => false) typargs;
  12.383        in
  12.384          thy
  12.385          |> class_interpretation class [def'] [def_eq]
  12.386 @@ -754,52 +845,4 @@
  12.387  
  12.388  end; (*local*)
  12.389  
  12.390 -(*experimental*)
  12.391 -fun class_term_check thy class =
  12.392 -  let
  12.393 -    val algebra = Sign.classes_of thy;
  12.394 -    val { v, ... } = the_class_data thy class;
  12.395 -    fun add_constrain_classtyp sort' (ty as TFree (v, _)) =
  12.396 -          AList.map_default (op =) (v, []) (curry (Sorts.inter_sort algebra) sort')
  12.397 -      | add_constrain_classtyp sort' (Type (tyco, tys)) = case Sorts.mg_domain algebra tyco sort'
  12.398 -         of sorts => fold2 add_constrain_classtyp sorts tys;
  12.399 -    fun class_arg c idx ty =
  12.400 -      let
  12.401 -        val typargs = Sign.const_typargs thy (c, ty);
  12.402 -        fun classtyp (t as TFree (w, _)) = if w = v then NONE else SOME t
  12.403 -          | classtyp t = SOME t;
  12.404 -      in classtyp (nth typargs idx) end;
  12.405 -    fun add_inst (c, ty) (terminsts, typinsts) = case local_param thy class c
  12.406 -     of NONE => (terminsts, typinsts)
  12.407 -      | SOME (t, (class', idx)) => (case class_arg c idx ty
  12.408 -         of NONE => (((c, ty), t) :: terminsts, typinsts)
  12.409 -          | SOME ty => (terminsts, add_constrain_classtyp [class'] ty typinsts));
  12.410 -  in pair o (fn ts => let
  12.411 -    val cs = (fold o fold_aterms) (fn Const c_ty => insert (op =) c_ty | _ => I) ts [];
  12.412 -    val (terminsts, typinsts) = fold add_inst cs ([], []);
  12.413 -  in
  12.414 -    ts
  12.415 -    |> (map o map_aterms) (fn t as Const c_ty => the_default t (AList.lookup (op =) terminsts c_ty)
  12.416 -         | t => t)
  12.417 -    |> (map o map_types o map_atyps) (fn t as TFree (v, sort) =>
  12.418 -         case AList.lookup (op =) typinsts v
  12.419 -          of SOME sort' => TFree (v, Sorts.inter_sort algebra (sort, sort'))
  12.420 -           | NONE => t)
  12.421 -  end) end;
  12.422 -
  12.423 -val init_ref = ref (K (pair I) : class -> Proof.context -> (theory -> theory) * Proof.context);
  12.424 -fun init class = ! init_ref class;
  12.425 -
  12.426 -fun init_default class ctxt =
  12.427 -  let
  12.428 -    val thy = ProofContext.theory_of ctxt;
  12.429 -    val term_check = class_term_check thy class;
  12.430 -  in
  12.431 -    ctxt
  12.432 -    (*|> ProofContext.theory_result (remove_constraints class)*)
  12.433 -    |> Context.proof_map (Syntax.add_term_check term_check)
  12.434 -    (*|>> fold (fn (c, ty) => Sign.add_const_constraint_i (c, SOME ty))*)
  12.435 -    |> pair I
  12.436 -  end;
  12.437 -
  12.438  end;
    13.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Sep 28 10:35:53 2007 +0200
    13.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Sep 29 08:58:51 2007 +0200
    13.3 @@ -415,14 +415,15 @@
    13.4    OuterSyntax.command "class" "define type class" K.thy_decl (
    13.5      P.name
    13.6      -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
    13.7 +    -- Scan.optional (P.$$$ "(" |-- (P.$$$ "local_syntax" >> K true) --| P.$$$ ")") false
    13.8      --| P.$$$ "=" -- (
    13.9        class_subP --| P.$$$ "+" -- class_bodyP
   13.10        || class_subP >> rpair []
   13.11        || class_bodyP >> pair [])
   13.12      -- P.opt_begin
   13.13 -    >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
   13.14 +    >> (fn ((((bname, add_consts), local_syntax), (supclasses, elems)), begin) =>
   13.15          Toplevel.begin_local_theory begin
   13.16 -          (Class.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
   13.17 +          (Class.class_cmd false bname supclasses elems add_consts #-> TheoryTarget.begin)));
   13.18  
   13.19  val instanceP =
   13.20    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
   13.21 @@ -985,7 +986,7 @@
   13.22    "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
   13.23    "constrains", "defines", "fixes", "for", "identifier", "if",
   13.24    "imports", "in", "includes", "infix", "infixl", "infixr", "is",
   13.25 -  "notes", "obtains", "open", "output", "overloaded", "shows",
   13.26 +  "local_syntax", "notes", "obtains", "open", "output", "overloaded", "shows",
   13.27    "structure", "unchecked", "uses", "where", "|"];
   13.28  
   13.29  val _ = OuterSyntax.add_parsers [
    14.1 --- a/src/Pure/Isar/theory_target.ML	Fri Sep 28 10:35:53 2007 +0200
    14.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Sep 29 08:58:51 2007 +0200
    14.3 @@ -359,15 +359,15 @@
    14.4      val thy = ProofContext.theory_of ctxt;
    14.5      val is_loc = loc <> "";
    14.6      val some_class = Class.class_of_locale thy loc;
    14.7 -    fun class_init_exit (SOME class) =
    14.8 -          Class.init class
    14.9 -      | class_init_exit NONE =
   14.10 -          pair I;
   14.11 +    fun class_init (SOME class) =
   14.12 +          Class.init [class]
   14.13 +      | class_init NONE =
   14.14 +          I;
   14.15    in
   14.16      ctxt
   14.17      |> Data.put (if is_loc then SOME loc else NONE)
   14.18 -    |> class_init_exit some_class
   14.19 -    |-> (fn exit => LocalTheory.init (NameSpace.base loc)
   14.20 +    |> class_init some_class
   14.21 +    |> LocalTheory.init (NameSpace.base loc)
   14.22       {pretty = pretty loc,
   14.23        consts = consts is_loc some_class,
   14.24        axioms = axioms,
   14.25 @@ -382,7 +382,7 @@
   14.26        reinit = fn _ =>
   14.27          (if is_loc then Locale.init loc else ProofContext.init)
   14.28          #> begin loc,
   14.29 -      exit = LocalTheory.target_of #> ProofContext.theory exit })
   14.30 +      exit = LocalTheory.target_of }
   14.31    end;
   14.32  
   14.33  fun init_i NONE thy = begin "" (ProofContext.init thy)