src/HOL/Algebra/UnivPoly.thy
 changeset 36092 8f1e60d9f7cc parent 34915 7894c7dab132 child 36096 abc6a2ea4b88
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Feb 11 21:00:36 2010 +0100
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Feb 15 01:27:06 2010 +0100
1.3 @@ -1342,14 +1342,8 @@
1.4  text {* Interpretation of ring homomorphism lemmas. *}
1.5
1.6  sublocale UP_univ_prop < ring_hom_cring P S Eval
1.7 -  apply (unfold Eval_def)
1.8 -  apply intro_locales
1.9 -  apply (rule ring_hom_cring.axioms)
1.10 -  apply (rule ring_hom_cring.intro)
1.11 -  apply unfold_locales
1.12 -  apply (rule eval_ring_hom)
1.13 -  apply rule
1.14 -  done
1.15 +  unfolding Eval_def
1.16 +  by unfold_locales (fast intro: eval_ring_hom)
1.17
1.18  lemma (in UP_cring) monom_pow:
1.19    assumes R: "a \<in> carrier R"
1.20 @@ -1436,10 +1430,7 @@
1.21  lemma ring_homD:
1.22    assumes Phi: "Phi \<in> ring_hom P S"
1.23    shows "ring_hom_cring P S Phi"
1.24 -proof (rule ring_hom_cring.intro)
1.25 -  show "ring_hom_cring_axioms P S Phi"
1.26 -  by (rule ring_hom_cring_axioms.intro) (rule Phi)
1.27 -qed unfold_locales
1.28 +  by unfold_locales (rule Phi)
1.29
1.30  theorem UP_universal_property:
1.31    assumes S: "s \<in> carrier S"
1.32 @@ -1759,9 +1750,9 @@
1.33    shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
1.34    (is "eval R R id a ?g = _")
1.35  proof -
1.36 -  interpret UP_pre_univ_prop R R id proof qed simp
1.37 +  interpret UP_pre_univ_prop R R id by unfold_locales simp
1.38    have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
1.39 -  interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom)
1.40 +  interpret ring_hom_cring P R "eval R R id a" by unfold_locales (rule eval_ring_hom)
1.41    have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P"
1.42      and mon0_closed: "monom P a 0 \<in> carrier P"
1.43      and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
```