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"