Conversion of HOL-Main and ZF to new locales.
authorballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223e09c53289830
parent 29208 b0c81b9a0133
child 29224 5226d990d74b
Conversion of HOL-Main and ZF to new locales.
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/Groebner_Basis.thy
src/HOL/Lattices.thy
src/HOL/List.thy
src/HOL/ex/LocaleTest2.thy
src/HOL/main.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/theory_target.ML
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Separation.thy
src/ZF/ROOT.ML
src/ZF/ex/Group.thy
src/ZF/ex/Ring.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -639,7 +639,7 @@
     1.4  
     1.5  text {* @{term "op dvd"} is a partial order *}
     1.6  
     1.7 -interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
     1.8 +class_interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
     1.9    proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
    1.10  
    1.11  lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
     2.1 --- a/src/HOL/Finite_Set.thy	Wed Dec 10 17:19:25 2008 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Thu Dec 11 18:30:26 2008 +0100
     2.3 @@ -750,7 +750,7 @@
     2.4  assumes "finite A" and "a \<notin> A"
     2.5  shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
     2.6  proof -
     2.7 -  interpret I: fun_left_comm ["%x y. (g x) * y"]
     2.8 +  interpret I: fun_left_comm "%x y. (g x) * y"
     2.9      by unfold_locales (simp add: mult_ac)
    2.10    show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
    2.11  qed
    2.12 @@ -798,7 +798,7 @@
    2.13      and hyp: "\<And>x y. h (g x y) = times x (h y)"
    2.14    shows "h (fold g j w A) = fold times j (h w) A"
    2.15  proof -
    2.16 -  interpret ab_semigroup_mult [g] by fact
    2.17 +  class_interpret ab_semigroup_mult [g] by fact
    2.18    show ?thesis using fin hyp by (induct set: finite) simp_all
    2.19  qed
    2.20  *)
    2.21 @@ -873,7 +873,7 @@
    2.22  
    2.23  subsection {* Generalized summation over a set *}
    2.24  
    2.25 -interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
    2.26 +class_interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
    2.27    proof qed (auto intro: add_assoc add_commute)
    2.28  
    2.29  definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
    2.30 @@ -1760,7 +1760,7 @@
    2.31  proof (induct rule: finite_induct)
    2.32    case empty then show ?case by simp
    2.33  next
    2.34 -  interpret ab_semigroup_mult ["op Un"]
    2.35 +  class_interpret ab_semigroup_mult ["op Un"]
    2.36      proof qed auto
    2.37    case insert 
    2.38    then show ?case by simp
    2.39 @@ -1943,7 +1943,7 @@
    2.40  assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
    2.41  shows "fold_graph times z (insert b A) (z * y)"
    2.42  proof -
    2.43 -  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
    2.44 +  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
    2.45  from assms show ?thesis
    2.46  proof (induct rule: fold_graph.induct)
    2.47    case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
    2.48 @@ -1983,7 +1983,7 @@
    2.49  lemma fold1_eq_fold:
    2.50  assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
    2.51  proof -
    2.52 -  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
    2.53 +  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
    2.54    from assms show ?thesis
    2.55  apply (simp add: fold1_def fold_def)
    2.56  apply (rule the_equality)
    2.57 @@ -2010,7 +2010,7 @@
    2.58    assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
    2.59    shows "fold1 times (insert x A) = x * fold1 times A"
    2.60  proof -
    2.61 -  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
    2.62 +  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
    2.63    from nonempty obtain a A' where "A = insert a A' & a ~: A'"
    2.64      by (auto simp add: nonempty_iff)
    2.65    with A show ?thesis
    2.66 @@ -2033,7 +2033,7 @@
    2.67    assumes nonempty: "A \<noteq> {}" and A: "finite A" 
    2.68    shows "fold1 times (insert x A) = x * fold1 times A"
    2.69  proof -
    2.70 -  interpret fun_left_comm_idem ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"]
    2.71 +  interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
    2.72      by (rule fun_left_comm_idem)
    2.73    from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
    2.74      by (auto simp add: nonempty_iff)
    2.75 @@ -2198,7 +2198,7 @@
    2.76    assumes "finite A" "A \<noteq> {}"
    2.77    shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
    2.78  proof -
    2.79 -  interpret ab_semigroup_idem_mult [inf]
    2.80 +  class_interpret ab_semigroup_idem_mult [inf]
    2.81      by (rule ab_semigroup_idem_mult_inf)
    2.82    show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
    2.83  qed
    2.84 @@ -2213,7 +2213,7 @@
    2.85    proof (induct rule: finite_ne_induct)
    2.86      case singleton thus ?case by simp
    2.87    next
    2.88 -    interpret ab_semigroup_idem_mult [inf]
    2.89 +    class_interpret ab_semigroup_idem_mult [inf]
    2.90        by (rule ab_semigroup_idem_mult_inf)
    2.91      case (insert x F)
    2.92      from insert(5) have "a = x \<or> a \<in> F" by simp
    2.93 @@ -2288,7 +2288,7 @@
    2.94      and "A \<noteq> {}"
    2.95    shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
    2.96  proof -
    2.97 -  interpret ab_semigroup_idem_mult [inf]
    2.98 +  class_interpret ab_semigroup_idem_mult [inf]
    2.99      by (rule ab_semigroup_idem_mult_inf)
   2.100    from assms show ?thesis
   2.101      by (simp add: Inf_fin_def image_def
   2.102 @@ -2303,7 +2303,7 @@
   2.103    case singleton thus ?case
   2.104      by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
   2.105  next
   2.106 -  interpret ab_semigroup_idem_mult [inf]
   2.107 +  class_interpret ab_semigroup_idem_mult [inf]
   2.108      by (rule ab_semigroup_idem_mult_inf)
   2.109    case (insert x A)
   2.110    have finB: "finite {sup x b |b. b \<in> B}"
   2.111 @@ -2333,7 +2333,7 @@
   2.112    assumes "finite A" and "A \<noteq> {}"
   2.113    shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
   2.114  proof -
   2.115 -  interpret ab_semigroup_idem_mult [sup]
   2.116 +  class_interpret ab_semigroup_idem_mult [sup]
   2.117      by (rule ab_semigroup_idem_mult_sup)
   2.118    from assms show ?thesis
   2.119      by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
   2.120 @@ -2357,7 +2357,7 @@
   2.121      thus ?thesis by(simp add: insert(1) B(1))
   2.122    qed
   2.123    have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   2.124 -  interpret ab_semigroup_idem_mult [sup]
   2.125 +  class_interpret ab_semigroup_idem_mult [sup]
   2.126      by (rule ab_semigroup_idem_mult_sup)
   2.127    have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
   2.128      using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
   2.129 @@ -2386,7 +2386,7 @@
   2.130    assumes "finite A" and "A \<noteq> {}"
   2.131    shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
   2.132  proof -
   2.133 -  interpret ab_semigroup_idem_mult [inf]
   2.134 +  class_interpret ab_semigroup_idem_mult [inf]
   2.135      by (rule ab_semigroup_idem_mult_inf)
   2.136    from assms show ?thesis
   2.137    unfolding Inf_fin_def by (induct A set: finite)
   2.138 @@ -2397,7 +2397,7 @@
   2.139    assumes "finite A" and "A \<noteq> {}"
   2.140    shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
   2.141  proof -
   2.142 -  interpret ab_semigroup_idem_mult [sup]
   2.143 +  class_interpret ab_semigroup_idem_mult [sup]
   2.144      by (rule ab_semigroup_idem_mult_sup)
   2.145    from assms show ?thesis
   2.146    unfolding Sup_fin_def by (induct A set: finite)
   2.147 @@ -2446,7 +2446,7 @@
   2.148    assumes "finite A" and "A \<noteq> {}"
   2.149    shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   2.150  proof -
   2.151 -  interpret ab_semigroup_idem_mult [min]
   2.152 +  class_interpret ab_semigroup_idem_mult [min]
   2.153      by (rule ab_semigroup_idem_mult_min)
   2.154    from assms show ?thesis
   2.155    by (induct rule: finite_ne_induct)
   2.156 @@ -2457,7 +2457,7 @@
   2.157    assumes "finite A" and "A \<noteq> {}"
   2.158    shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   2.159  proof -
   2.160 -  interpret ab_semigroup_idem_mult [min]
   2.161 +  class_interpret ab_semigroup_idem_mult [min]
   2.162      by (rule ab_semigroup_idem_mult_min)
   2.163    from assms show ?thesis
   2.164    by (induct rule: finite_ne_induct)
   2.165 @@ -2468,7 +2468,7 @@
   2.166    assumes "finite A" and "A \<noteq> {}"
   2.167    shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   2.168  proof -
   2.169 -  interpret ab_semigroup_idem_mult [min]
   2.170 +  class_interpret ab_semigroup_idem_mult [min]
   2.171      by (rule ab_semigroup_idem_mult_min)
   2.172    from assms show ?thesis
   2.173    by (induct rule: finite_ne_induct)
   2.174 @@ -2481,7 +2481,7 @@
   2.175  proof cases
   2.176    assume "A = B" thus ?thesis by simp
   2.177  next
   2.178 -  interpret ab_semigroup_idem_mult [min]
   2.179 +  class_interpret ab_semigroup_idem_mult [min]
   2.180      by (rule ab_semigroup_idem_mult_min)
   2.181    assume "A \<noteq> B"
   2.182    have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
   2.183 @@ -2515,7 +2515,7 @@
   2.184    assumes "finite A" and "A \<noteq> {}"
   2.185    shows "Min (insert x A) = min x (Min A)"
   2.186  proof -
   2.187 -  interpret ab_semigroup_idem_mult [min]
   2.188 +  class_interpret ab_semigroup_idem_mult [min]
   2.189      by (rule ab_semigroup_idem_mult_min)
   2.190    from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
   2.191  qed
   2.192 @@ -2524,7 +2524,7 @@
   2.193    assumes "finite A" and "A \<noteq> {}"
   2.194    shows "Max (insert x A) = max x (Max A)"
   2.195  proof -
   2.196 -  interpret ab_semigroup_idem_mult [max]
   2.197 +  class_interpret ab_semigroup_idem_mult [max]
   2.198      by (rule ab_semigroup_idem_mult_max)
   2.199    from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
   2.200  qed
   2.201 @@ -2533,7 +2533,7 @@
   2.202    assumes "finite A" and "A \<noteq> {}"
   2.203    shows "Min A \<in> A"
   2.204  proof -
   2.205 -  interpret ab_semigroup_idem_mult [min]
   2.206 +  class_interpret ab_semigroup_idem_mult [min]
   2.207      by (rule ab_semigroup_idem_mult_min)
   2.208    from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
   2.209  qed
   2.210 @@ -2542,7 +2542,7 @@
   2.211    assumes "finite A" and "A \<noteq> {}"
   2.212    shows "Max A \<in> A"
   2.213  proof -
   2.214 -  interpret ab_semigroup_idem_mult [max]
   2.215 +  class_interpret ab_semigroup_idem_mult [max]
   2.216      by (rule ab_semigroup_idem_mult_max)
   2.217    from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
   2.218  qed
   2.219 @@ -2551,7 +2551,7 @@
   2.220    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   2.221    shows "Min (A \<union> B) = min (Min A) (Min B)"
   2.222  proof -
   2.223 -  interpret ab_semigroup_idem_mult [min]
   2.224 +  class_interpret ab_semigroup_idem_mult [min]
   2.225      by (rule ab_semigroup_idem_mult_min)
   2.226    from assms show ?thesis
   2.227      by (simp add: Min_def fold1_Un2)
   2.228 @@ -2561,7 +2561,7 @@
   2.229    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   2.230    shows "Max (A \<union> B) = max (Max A) (Max B)"
   2.231  proof -
   2.232 -  interpret ab_semigroup_idem_mult [max]
   2.233 +  class_interpret ab_semigroup_idem_mult [max]
   2.234      by (rule ab_semigroup_idem_mult_max)
   2.235    from assms show ?thesis
   2.236      by (simp add: Max_def fold1_Un2)
   2.237 @@ -2572,7 +2572,7 @@
   2.238      and "finite N" and "N \<noteq> {}"
   2.239    shows "h (Min N) = Min (h ` N)"
   2.240  proof -
   2.241 -  interpret ab_semigroup_idem_mult [min]
   2.242 +  class_interpret ab_semigroup_idem_mult [min]
   2.243      by (rule ab_semigroup_idem_mult_min)
   2.244    from assms show ?thesis
   2.245      by (simp add: Min_def hom_fold1_commute)
   2.246 @@ -2583,7 +2583,7 @@
   2.247      and "finite N" and "N \<noteq> {}"
   2.248    shows "h (Max N) = Max (h ` N)"
   2.249  proof -
   2.250 -  interpret ab_semigroup_idem_mult [max]
   2.251 +  class_interpret ab_semigroup_idem_mult [max]
   2.252      by (rule ab_semigroup_idem_mult_max)
   2.253    from assms show ?thesis
   2.254      by (simp add: Max_def hom_fold1_commute [of h])
   2.255 @@ -2593,7 +2593,7 @@
   2.256    assumes "finite A" and "x \<in> A"
   2.257    shows "Min A \<le> x"
   2.258  proof -
   2.259 -  interpret lower_semilattice ["op \<le>" "op <" min]
   2.260 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
   2.261      by (rule min_lattice)
   2.262    from assms show ?thesis by (simp add: Min_def fold1_belowI)
   2.263  qed
   2.264 @@ -2611,7 +2611,7 @@
   2.265    assumes "finite A" and "A \<noteq> {}"
   2.266    shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   2.267  proof -
   2.268 -  interpret lower_semilattice ["op \<le>" "op <" min]
   2.269 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
   2.270      by (rule min_lattice)
   2.271    from assms show ?thesis by (simp add: Min_def below_fold1_iff)
   2.272  qed
   2.273 @@ -2629,7 +2629,7 @@
   2.274    assumes "finite A" and "A \<noteq> {}"
   2.275    shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   2.276  proof -
   2.277 -  interpret lower_semilattice ["op \<le>" "op <" min]
   2.278 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
   2.279      by (rule min_lattice)
   2.280    from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
   2.281  qed
   2.282 @@ -2639,7 +2639,7 @@
   2.283    shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   2.284  proof -
   2.285    note Max = Max_def
   2.286 -  interpret linorder ["op \<ge>" "op >"]
   2.287 +  class_interpret linorder ["op \<ge>" "op >"]
   2.288      by (rule dual_linorder)
   2.289    from assms show ?thesis
   2.290      by (simp add: Max strict_below_fold1_iff [folded dual_max])
   2.291 @@ -2649,7 +2649,7 @@
   2.292    assumes "finite A" and "A \<noteq> {}"
   2.293    shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   2.294  proof -
   2.295 -  interpret lower_semilattice ["op \<le>" "op <" min]
   2.296 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
   2.297      by (rule min_lattice)
   2.298    from assms show ?thesis
   2.299      by (simp add: Min_def fold1_below_iff)
   2.300 @@ -2660,7 +2660,7 @@
   2.301    shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   2.302  proof -
   2.303    note Max = Max_def
   2.304 -  interpret linorder ["op \<ge>" "op >"]
   2.305 +  class_interpret linorder ["op \<ge>" "op >"]
   2.306      by (rule dual_linorder)
   2.307    from assms show ?thesis
   2.308      by (simp add: Max fold1_below_iff [folded dual_max])
   2.309 @@ -2670,7 +2670,7 @@
   2.310    assumes "finite A" and "A \<noteq> {}"
   2.311    shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   2.312  proof -
   2.313 -  interpret lower_semilattice ["op \<le>" "op <" min]
   2.314 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
   2.315      by (rule min_lattice)
   2.316    from assms show ?thesis
   2.317      by (simp add: Min_def fold1_strict_below_iff)
   2.318 @@ -2681,7 +2681,7 @@
   2.319    shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   2.320  proof -
   2.321    note Max = Max_def
   2.322 -  interpret linorder ["op \<ge>" "op >"]
   2.323 +  class_interpret linorder ["op \<ge>" "op >"]
   2.324      by (rule dual_linorder)
   2.325    from assms show ?thesis
   2.326      by (simp add: Max fold1_strict_below_iff [folded dual_max])
   2.327 @@ -2691,7 +2691,7 @@
   2.328    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   2.329    shows "Min N \<le> Min M"
   2.330  proof -
   2.331 -  interpret distrib_lattice ["op \<le>" "op <" min max]
   2.332 +  class_interpret distrib_lattice ["op \<le>" "op <" min max]
   2.333      by (rule distrib_lattice_min_max)
   2.334    from assms show ?thesis by (simp add: Min_def fold1_antimono)
   2.335  qed
   2.336 @@ -2701,7 +2701,7 @@
   2.337    shows "Max M \<le> Max N"
   2.338  proof -
   2.339    note Max = Max_def
   2.340 -  interpret linorder ["op \<ge>" "op >"]
   2.341 +  class_interpret linorder ["op \<ge>" "op >"]
   2.342      by (rule dual_linorder)
   2.343    from assms show ?thesis
   2.344      by (simp add: Max fold1_antimono [folded dual_max])
     3.1 --- a/src/HOL/Groebner_Basis.thy	Wed Dec 10 17:19:25 2008 +0100
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Dec 11 18:30:26 2008 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOL/Groebner_Basis.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Amine Chaieb, TU Muenchen
     3.7  *)
     3.8  
     3.9 @@ -165,7 +164,7 @@
    3.10  end
    3.11  
    3.12  interpretation class_semiring: gb_semiring
    3.13 -    ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
    3.14 +    "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
    3.15    proof qed (auto simp add: ring_simps power_Suc)
    3.16  
    3.17  lemmas nat_arith =
    3.18 @@ -242,8 +241,8 @@
    3.19  end
    3.20  
    3.21  
    3.22 -interpretation class_ring: gb_ring ["op +" "op *" "op ^"
    3.23 -    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
    3.24 +interpretation class_ring: gb_ring "op +" "op *" "op ^"
    3.25 +    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
    3.26    proof qed simp_all
    3.27  
    3.28  
    3.29 @@ -344,7 +343,7 @@
    3.30  qed
    3.31  
    3.32  interpretation class_ringb: ringb
    3.33 -  ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
    3.34 +  "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
    3.35  proof(unfold_locales, simp add: ring_simps power_Suc, auto)
    3.36    fix w x y z ::"'a::{idom,recpower,number_ring}"
    3.37    assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    3.38 @@ -360,7 +359,7 @@
    3.39  declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
    3.40  
    3.41  interpretation natgb: semiringb
    3.42 -  ["op +" "op *" "op ^" "0::nat" "1"]
    3.43 +  "op +" "op *" "op ^" "0::nat" "1"
    3.44  proof (unfold_locales, simp add: ring_simps power_Suc)
    3.45    fix w x y z ::"nat"
    3.46    { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    3.47 @@ -465,7 +464,7 @@
    3.48  subsection{* Groebner Bases for fields *}
    3.49  
    3.50  interpretation class_fieldgb:
    3.51 -  fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse)
    3.52 +  fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
    3.53  
    3.54  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
    3.55  lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
     4.1 --- a/src/HOL/Lattices.thy	Wed Dec 10 17:19:25 2008 +0100
     4.2 +++ b/src/HOL/Lattices.thy	Thu Dec 11 18:30:26 2008 +0100
     4.3 @@ -300,7 +300,7 @@
     4.4    by auto
     4.5  qed (auto simp add: min_def max_def not_le less_imp_le)
     4.6  
     4.7 -interpretation min_max:
     4.8 +class_interpretation min_max:
     4.9    distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
    4.10    by (rule distrib_lattice_min_max)
    4.11  
     5.1 --- a/src/HOL/List.thy	Wed Dec 10 17:19:25 2008 +0100
     5.2 +++ b/src/HOL/List.thy	Thu Dec 11 18:30:26 2008 +0100
     5.3 @@ -548,9 +548,9 @@
     5.4  lemma append_Nil2 [simp]: "xs @ [] = xs"
     5.5  by (induct xs) auto
     5.6  
     5.7 -interpretation semigroup_append: semigroup_add ["op @"]
     5.8 +class_interpretation semigroup_append: semigroup_add ["op @"]
     5.9    proof qed simp
    5.10 -interpretation monoid_append: monoid_add ["[]" "op @"]
    5.11 +class_interpretation monoid_append: monoid_add ["[]" "op @"]
    5.12    proof qed simp+
    5.13  
    5.14  lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
     6.1 --- a/src/HOL/ex/LocaleTest2.thy	Wed Dec 10 17:19:25 2008 +0100
     6.2 +++ b/src/HOL/ex/LocaleTest2.thy	Thu Dec 11 18:30:26 2008 +0100
     6.3 @@ -433,8 +433,7 @@
     6.4  end
     6.5  
     6.6  
     6.7 -interpretation dlo < dlat
     6.8 -(* TODO: definition syntax is unavailable *)
     6.9 +sublocale dlo < dlat
    6.10  proof
    6.11    fix x y
    6.12    from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
    6.13 @@ -445,7 +444,7 @@
    6.14    then show "EX sup. is_sup x y sup" by blast
    6.15  qed
    6.16  
    6.17 -interpretation dlo < ddlat
    6.18 +sublocale dlo < ddlat
    6.19  proof
    6.20    fix x y z
    6.21    show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
     7.1 --- a/src/HOL/main.ML	Wed Dec 10 17:19:25 2008 +0100
     7.2 +++ b/src/HOL/main.ML	Thu Dec 11 18:30:26 2008 +0100
     7.3 @@ -4,4 +4,5 @@
     7.4  Classical Higher-order Logic -- only "Main".
     7.5  *)
     7.6  
     7.7 +set new_locales;
     7.8  use_thy "Main";
     8.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 10 17:19:25 2008 +0100
     8.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Dec 11 18:30:26 2008 +0100
     8.3 @@ -53,8 +53,7 @@
     8.4    val print_configs: Toplevel.transition -> Toplevel.transition
     8.5    val print_theorems: Toplevel.transition -> Toplevel.transition
     8.6    val print_locales: Toplevel.transition -> Toplevel.transition
     8.7 -  val print_locale: bool * (Locale.expr * Element.context list)
     8.8 -    -> Toplevel.transition -> Toplevel.transition
     8.9 +  val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
    8.10    val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
    8.11    val print_attributes: Toplevel.transition -> Toplevel.transition
    8.12    val print_simpset: Toplevel.transition -> Toplevel.transition
    8.13 @@ -354,11 +353,11 @@
    8.14  val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
    8.15  
    8.16  val print_locales = Toplevel.unknown_theory o
    8.17 -  Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
    8.18 +  Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of);
    8.19  
    8.20 -fun print_locale (show_facts, (imports, body)) = Toplevel.unknown_theory o
    8.21 +fun print_locale (show_facts, name) = Toplevel.unknown_theory o
    8.22    Toplevel.keep (fn state =>
    8.23 -    Locale.print_locale (Toplevel.theory_of state) show_facts imports body);
    8.24 +    NewLocale.print_locale (Toplevel.theory_of state) show_facts name);
    8.25  
    8.26  fun print_registrations show_wits name = Toplevel.unknown_context o
    8.27    Toplevel.keep (Toplevel.node_case
     9.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Dec 10 17:19:25 2008 +0100
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Dec 11 18:30:26 2008 +0100
     9.3 @@ -385,18 +385,18 @@
     9.4  (* locales *)
     9.5  
     9.6  val locale_val =
     9.7 -  SpecParse.locale_expr --
     9.8 +  SpecParse.locale_expression --
     9.9      Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
    9.10 -  Scan.repeat1 SpecParse.context_element >> pair Locale.empty;
    9.11 +  Scan.repeat1 SpecParse.context_element >> pair ([], []);
    9.12  
    9.13  val _ =
    9.14    OuterSyntax.command "locale" "define named proof context" K.thy_decl
    9.15 -    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
    9.16 +    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
    9.17        >> (fn ((name, (expr, elems)), begin) =>
    9.18            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
    9.19 -            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
    9.20 -
    9.21 -val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
    9.22 +            (Expression.add_locale_cmd name name expr elems #>
    9.23 +              (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |>
    9.24 +                fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes))));
    9.25  
    9.26  val _ =
    9.27    OuterSyntax.command "sublocale"
    9.28 @@ -407,6 +407,39 @@
    9.29  
    9.30  val _ =
    9.31    OuterSyntax.command "interpretation"
    9.32 +    "prove interpretation of locale expression in theory" K.thy_goal
    9.33 +    (P.!!! SpecParse.locale_expression
    9.34 +        >> (fn expr => Toplevel.print o
    9.35 +            Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
    9.36 +
    9.37 +val _ =
    9.38 +  OuterSyntax.command "interpret"
    9.39 +    "prove interpretation of locale expression in proof context"
    9.40 +    (K.tag_proof K.prf_goal)
    9.41 +    (P.!!! SpecParse.locale_expression
    9.42 +        >> (fn expr => Toplevel.print o
    9.43 +            Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
    9.44 +
    9.45 +local
    9.46 +
    9.47 +val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
    9.48 +
    9.49 +in
    9.50 +
    9.51 +val locale_val =
    9.52 +  SpecParse.locale_expr --
    9.53 +    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
    9.54 +  Scan.repeat1 SpecParse.context_element >> pair Locale.empty;
    9.55 +
    9.56 +val _ =
    9.57 +  OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl
    9.58 +    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
    9.59 +      >> (fn ((name, (expr, elems)), begin) =>
    9.60 +          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
    9.61 +            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
    9.62 +
    9.63 +val _ =
    9.64 +  OuterSyntax.command "class_interpretation"
    9.65      "prove and register interpretation of locale expression in theory or locale" K.thy_goal
    9.66      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
    9.67        >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
    9.68 @@ -416,7 +449,7 @@
    9.69                (Locale.interpretation_cmd (Binding.base_name name) expr insts)));
    9.70  
    9.71  val _ =
    9.72 -  OuterSyntax.command "interpret"
    9.73 +  OuterSyntax.command "class_interpret"
    9.74      "prove and register interpretation of locale expression in proof context"
    9.75      (K.tag_proof K.prf_goal)
    9.76      (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
    9.77 @@ -424,6 +457,8 @@
    9.78            Toplevel.proof'
    9.79              (fn int => Locale.interpret_cmd (Binding.base_name name) expr insts int)));
    9.80  
    9.81 +end;
    9.82 +
    9.83  
    9.84  (* classes *)
    9.85  
    9.86 @@ -817,7 +852,7 @@
    9.87  
    9.88  val _ =
    9.89    OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
    9.90 -    (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
    9.91 +    (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
    9.92  
    9.93  val _ =
    9.94    OuterSyntax.improper_command "print_interps"
    10.1 --- a/src/Pure/Isar/theory_target.ML	Wed Dec 10 17:19:25 2008 +0100
    10.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Dec 11 18:30:26 2008 +0100
    10.3 @@ -24,13 +24,20 @@
    10.4  
    10.5  (* new locales *)
    10.6  
    10.7 -fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x;
    10.8 -fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    10.9 -fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
   10.10 -fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
   10.11 -fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
   10.12 -fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x;
   10.13 -fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x;
   10.14 +fun locale_extern is_class x = 
   10.15 +  if !new_locales andalso not is_class then NewLocale.extern x else Locale.extern x;
   10.16 +fun locale_add_type_syntax is_class x =
   10.17 +  if !new_locales andalso not is_class then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
   10.18 +fun locale_add_term_syntax is_class x =
   10.19 +  if !new_locales andalso not is_class then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
   10.20 +fun locale_add_declaration is_class x =
   10.21 +  if !new_locales andalso not is_class then NewLocale.add_declaration x else Locale.add_declaration x;
   10.22 +fun locale_add_thmss is_class x =
   10.23 +  if !new_locales andalso not is_class then NewLocale.add_thmss x else Locale.add_thmss x;
   10.24 +fun locale_init x =
   10.25 +  if !new_locales then NewLocale.init x else Locale.init x;
   10.26 +fun locale_intern is_class x =
   10.27 +  if !new_locales andalso not is_class then NewLocale.intern x else Locale.intern x;
   10.28  
   10.29  (* context data *)
   10.30  
   10.31 @@ -58,7 +65,7 @@
   10.32  fun pretty_thy ctxt target is_locale is_class =
   10.33    let
   10.34      val thy = ProofContext.theory_of ctxt;
   10.35 -    val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
   10.36 +    val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target;
   10.37      val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
   10.38        (#1 (ProofContext.inferred_fixes ctxt));
   10.39      val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
   10.40 @@ -94,7 +101,7 @@
   10.41        |> LocalTheory.target (Context.proof_map d0)
   10.42      else
   10.43        lthy
   10.44 -      |> LocalTheory.target (add target d')
   10.45 +      |> LocalTheory.target (add is_class target d')
   10.46    end;
   10.47  
   10.48  val type_syntax = target_decl locale_add_type_syntax;
   10.49 @@ -179,7 +186,7 @@
   10.50          #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
   10.51          #> Sign.restore_naming thy)
   10.52      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
   10.53 -    |> is_locale ? LocalTheory.target (locale_add_thmss target kind target_facts)
   10.54 +    |> is_locale ? LocalTheory.target (locale_add_thmss is_class target kind target_facts)
   10.55      |> note_local kind local_facts
   10.56    end;
   10.57  
   10.58 @@ -367,7 +374,8 @@
   10.59  fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
   10.60  
   10.61  fun context "-" thy = init NONE thy
   10.62 -  | context target thy = init (SOME (locale_intern thy target)) thy;
   10.63 +  | context target thy = init (SOME (locale_intern
   10.64 +      (not (NewLocale.test_locale thy (NewLocale.intern thy target))) thy target)) thy;
   10.65  
   10.66  fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
   10.67  
    11.1 --- a/src/ZF/Constructible/L_axioms.thy	Wed Dec 10 17:19:25 2008 +0100
    11.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Dec 11 18:30:26 2008 +0100
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      ZF/Constructible/L_axioms.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7  *)
    11.8  
    11.9 @@ -100,7 +99,7 @@
   11.10    apply (rule L_nat)
   11.11    done
   11.12  
   11.13 -interpretation M_trivial ["L"] by (rule M_trivial_L)
   11.14 +interpretation L: M_trivial L by (rule M_trivial_L)
   11.15  
   11.16  (* Replaces the following declarations...
   11.17  lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
    12.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Dec 10 17:19:25 2008 +0100
    12.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Dec 11 18:30:26 2008 +0100
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      ZF/Constructible/Rec_Separation.thy
    12.5 -    ID:   $Id$
    12.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7  *)
    12.8  
    12.9 @@ -186,7 +185,7 @@
   12.10  theorem M_trancl_L: "PROP M_trancl(L)"
   12.11  by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
   12.12  
   12.13 -interpretation M_trancl [L] by (rule M_trancl_L)
   12.14 +interpretation L: M_trancl L by (rule M_trancl_L)
   12.15  
   12.16  
   12.17  subsection{*@{term L} is Closed Under the Operator @{term list}*}
   12.18 @@ -373,7 +372,7 @@
   12.19    apply (rule M_datatypes_axioms_L) 
   12.20    done
   12.21  
   12.22 -interpretation M_datatypes [L] by (rule M_datatypes_L)
   12.23 +interpretation L: M_datatypes L by (rule M_datatypes_L)
   12.24  
   12.25  
   12.26  subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
   12.27 @@ -436,7 +435,7 @@
   12.28    apply (rule M_eclose_axioms_L)
   12.29    done
   12.30  
   12.31 -interpretation M_eclose [L] by (rule M_eclose_L)
   12.32 +interpretation L: M_eclose L by (rule M_eclose_L)
   12.33  
   12.34  
   12.35  end
    13.1 --- a/src/ZF/Constructible/Separation.thy	Wed Dec 10 17:19:25 2008 +0100
    13.2 +++ b/src/ZF/Constructible/Separation.thy	Thu Dec 11 18:30:26 2008 +0100
    13.3 @@ -305,7 +305,7 @@
    13.4  theorem M_basic_L: "PROP M_basic(L)"
    13.5  by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
    13.6  
    13.7 -interpretation M_basic [L] by (rule M_basic_L)
    13.8 +interpretation L: M_basic L by (rule M_basic_L)
    13.9  
   13.10  
   13.11  end
    14.1 --- a/src/ZF/ROOT.ML	Wed Dec 10 17:19:25 2008 +0100
    14.2 +++ b/src/ZF/ROOT.ML	Thu Dec 11 18:30:26 2008 +0100
    14.3 @@ -8,5 +8,6 @@
    14.4  Paulson.
    14.5  *)
    14.6  
    14.7 +set new_locales;
    14.8  use_thys ["Main", "Main_ZFC"];
    14.9  
    15.1 --- a/src/ZF/ex/Group.thy	Wed Dec 10 17:19:25 2008 +0100
    15.2 +++ b/src/ZF/ex/Group.thy	Thu Dec 11 18:30:26 2008 +0100
    15.3 @@ -1,5 +1,4 @@
    15.4  (* Title:  ZF/ex/Group.thy
    15.5 -  Id:     $Id$
    15.6  
    15.7  *)
    15.8  
    15.9 @@ -40,7 +39,7 @@
   15.10    m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where
   15.11    "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"
   15.12  
   15.13 -locale monoid = struct G +
   15.14 +locale monoid = fixes G (structure)
   15.15    assumes m_closed [intro, simp]:
   15.16           "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
   15.17        and m_assoc:
   15.18 @@ -242,7 +241,7 @@
   15.19  
   15.20  subsection {* Substructures *}
   15.21  
   15.22 -locale subgroup = var H + struct G + 
   15.23 +locale subgroup = fixes H and G (structure)
   15.24    assumes subset: "H \<subseteq> carrier(G)"
   15.25      and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H"
   15.26      and  one_closed [simp]: "\<one> \<in> H"
   15.27 @@ -262,7 +261,7 @@
   15.28    assumes "group(G)"
   15.29    shows "group_axioms (update_carrier(G,H))"
   15.30  proof -
   15.31 -  interpret group [G] by fact
   15.32 +  interpret group G by fact
   15.33    show ?thesis by (force intro: group_axioms.intro l_inv r_inv)
   15.34  qed
   15.35  
   15.36 @@ -270,7 +269,7 @@
   15.37    assumes "group(G)"
   15.38    shows "group (update_carrier(G,H))"
   15.39  proof -
   15.40 -  interpret group [G] by fact
   15.41 +  interpret group G by fact
   15.42    show ?thesis
   15.43    by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
   15.44  qed
   15.45 @@ -316,8 +315,8 @@
   15.46    assumes "group(G)" and "group(H)"
   15.47    shows "group (G \<Otimes> H)"
   15.48  proof -
   15.49 -  interpret G: group [G] by fact
   15.50 -  interpret H: group [H] by fact
   15.51 +  interpret G: group G by fact
   15.52 +  interpret H: group H by fact
   15.53    show ?thesis by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
   15.54            simp add: DirProdGroup_def)
   15.55  qed
   15.56 @@ -397,8 +396,8 @@
   15.57    assumes "group(G)" and "group(H)"
   15.58    shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
   15.59  proof -
   15.60 -  interpret group [G] by fact
   15.61 -  interpret group [H] by fact
   15.62 +  interpret group G by fact
   15.63 +  interpret group H by fact
   15.64    show ?thesis by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
   15.65  qed
   15.66  
   15.67 @@ -407,16 +406,17 @@
   15.68    shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
   15.69            \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
   15.70  proof -
   15.71 -  interpret group [G] by fact
   15.72 -  interpret group [H] by fact
   15.73 -  interpret group [I] by fact
   15.74 +  interpret group G by fact
   15.75 +  interpret group H by fact
   15.76 +  interpret group I by fact
   15.77    show ?thesis
   15.78      by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) 
   15.79  qed
   15.80  
   15.81  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   15.82    @term{H}, with a homomorphism @{term h} between them*}
   15.83 -locale group_hom = group G + group H + var h +
   15.84 +locale group_hom = G: group G + H: group H
   15.85 +  for G (structure) and H (structure) and h +
   15.86    assumes homh: "h \<in> hom(G,H)"
   15.87    notes hom_mult [simp] = hom_mult [OF homh]
   15.88      and hom_closed [simp] = hom_closed [OF homh]
   15.89 @@ -870,7 +870,7 @@
   15.90     assumes "group(G)"
   15.91     shows "equiv (carrier(G), rcong H)"
   15.92  proof -
   15.93 -  interpret group [G] by fact
   15.94 +  interpret group G by fact
   15.95    show ?thesis proof (simp add: equiv_def, intro conjI)
   15.96      show "rcong H \<subseteq> carrier(G) \<times> carrier(G)"
   15.97        by (auto simp add: r_congruent_def) 
   15.98 @@ -907,7 +907,7 @@
   15.99    assumes a: "a \<in> carrier(G)"
  15.100    shows "a <# H = (rcong H) `` {a}" 
  15.101  proof -
  15.102 -  interpret group [G] by fact
  15.103 +  interpret group G by fact
  15.104    show ?thesis
  15.105      by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a
  15.106        Collect_image_eq) 
  15.107 @@ -920,7 +920,7 @@
  15.108          h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
  15.109        \<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})" (is "PROP ?P")
  15.110  proof -
  15.111 -  interpret subgroup [H G] by fact
  15.112 +  interpret subgroup H G by fact
  15.113    show "PROP ?P"
  15.114      apply (rule UN_I [of "hb \<cdot> ((inv ha) \<cdot> h)"], simp)
  15.115      apply (simp add: m_assoc transpose_inv)
  15.116 @@ -931,7 +931,7 @@
  15.117    assumes "subgroup(H, G)"
  15.118    shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = 0" (is "PROP ?P")
  15.119  proof -
  15.120 -  interpret subgroup [H G] by fact
  15.121 +  interpret subgroup H G by fact
  15.122    show "PROP ?P"
  15.123      apply (simp add: RCOSETS_def r_coset_def)
  15.124      apply (blast intro: rcos_equation prems sym)
  15.125 @@ -949,7 +949,7 @@
  15.126    assumes "subgroup(H, G)"
  15.127    shows "x \<in> carrier(G) \<Longrightarrow> x \<in> H #> x" (is "PROP ?P")
  15.128  proof -
  15.129 -  interpret subgroup [H G] by fact
  15.130 +  interpret subgroup H G by fact
  15.131    show "PROP ?P"
  15.132      apply (simp add: r_coset_def)
  15.133      apply (rule_tac x="\<one>" in bexI) apply (auto)
  15.134 @@ -960,7 +960,7 @@
  15.135    assumes "subgroup(H, G)"
  15.136    shows "\<Union>(rcosets H) = carrier(G)"
  15.137  proof -
  15.138 -  interpret subgroup [H G] by fact
  15.139 +  interpret subgroup H G by fact
  15.140    show ?thesis
  15.141      apply (rule equalityI)
  15.142      apply (force simp add: RCOSETS_def r_coset_def)
  15.143 @@ -1044,7 +1044,7 @@
  15.144    assumes "group(G)"
  15.145    shows "H \<in> rcosets H"
  15.146  proof -
  15.147 -  interpret group [G] by fact
  15.148 +  interpret group G by fact
  15.149    have "H #> \<one> = H"
  15.150      using _ subgroup_axioms by (rule coset_join2) simp_all
  15.151    then show ?thesis
    16.1 --- a/src/ZF/ex/Ring.thy	Wed Dec 10 17:19:25 2008 +0100
    16.2 +++ b/src/ZF/ex/Ring.thy	Thu Dec 11 18:30:26 2008 +0100
    16.3 @@ -45,7 +45,7 @@
    16.4    minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
    16.5    "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
    16.6  
    16.7 -locale abelian_monoid = struct G +
    16.8 +locale abelian_monoid = fixes G (structure)
    16.9    assumes a_comm_monoid: 
   16.10      "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
   16.11  
   16.12 @@ -57,7 +57,7 @@
   16.13    assumes a_comm_group: 
   16.14      "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
   16.15  
   16.16 -locale ring = abelian_group R + monoid R +
   16.17 +locale ring = abelian_group R + monoid R for R (structure) +
   16.18    assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
   16.19        \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
   16.20      and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
   16.21 @@ -262,7 +262,8 @@
   16.22  lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
   16.23  by (simp add: ring_hom_def)
   16.24  
   16.25 -locale ring_hom_cring = cring R + cring S + var h +
   16.26 +locale ring_hom_cring = R: cring R + S: cring S
   16.27 +  for R (structure) and S (structure) and h +
   16.28    assumes homh [simp, intro]: "h \<in> ring_hom(R,S)"
   16.29    notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
   16.30      and hom_mult [simp] = ring_hom_mult [OF homh]