More porting to new locales.
--- a/src/HOL/Algebra/RingHom.thy Fri Dec 19 14:31:07 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy Fri Dec 19 14:31:17 2008 +0100
@@ -17,10 +17,10 @@
notes hom_mult [simp] = ring_hom_mult [OF homh]
and hom_one [simp] = ring_hom_one [OF homh]
-sublocale ring_hom_cring \<subseteq> ring_hom_ring
+sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
proof qed (rule homh)
-sublocale ring_hom_ring \<subseteq> abelian_group_hom R S
+sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
apply (rule abelian_group_homI)
apply (rule R.is_abelian_group)
apply (rule S.is_abelian_group)
--- a/src/HOL/Algebra/UnivPoly.thy Fri Dec 19 14:31:07 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Dec 19 14:31:17 2008 +0100
@@ -1773,7 +1773,7 @@
shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
(is "eval R R id a ?g = _")
proof -
- interpret UP_pre_univ_prop R R id P proof qed simp
+ interpret UP_pre_univ_prop R R id proof qed simp
have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom)
have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P"
@@ -1782,8 +1782,8 @@
using a R.a_inv_closed by auto
have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
unfolding P.minus_eq [OF mon1_closed mon0_closed]
- unfolding R_S_h.hom_add [OF mon1_closed min_mon0_closed]
- unfolding R_S_h.hom_a_inv [OF mon0_closed]
+ unfolding hom_add [OF mon1_closed min_mon0_closed]
+ unfolding hom_a_inv [OF mon0_closed]
using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
also have "\<dots> = a \<ominus> a"
using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
@@ -1886,7 +1886,7 @@
"UP INTEG"} globally.
*}
-interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id
+interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
using INTEG_id_eval by simp_all
lemma INTEG_closed [intro, simp]: