src/HOL/Algebra/UnivPoly.thy
changeset 19984 29bb4659f80a
parent 19931 fb32b43e7f80
child 20217 25b068a99d2b
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Jul 04 12:13:38 2006 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Tue Jul 04 14:47:01 2006 +0200
     1.3 @@ -397,7 +397,7 @@
     1.4  *}
     1.5  
     1.6  interpretation UP_cring < cring P
     1.7 -  by (intro_locales!)
     1.8 +  by intro_locales
     1.9      (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms UP_cring)+
    1.10  
    1.11  
    1.12 @@ -441,7 +441,7 @@
    1.13      UP_smult_assoc1 UP_smult_assoc2)
    1.14  
    1.15  interpretation UP_cring < algebra R P
    1.16 -  by (intro_locales!)
    1.17 +  by intro_locales
    1.18      (rule module.axioms algebra.axioms UP_algebra)+
    1.19  
    1.20  
    1.21 @@ -945,7 +945,7 @@
    1.22  *}
    1.23  
    1.24  interpretation UP_domain < "domain" P
    1.25 -  by (intro_locales!) (rule domain.axioms UP_domain)+
    1.26 +  by intro_locales (rule domain.axioms UP_domain)+
    1.27  
    1.28  
    1.29  subsection {* Evaluation Homomorphism and Universal Property*}
    1.30 @@ -1148,10 +1148,10 @@
    1.31  
    1.32  interpretation UP_univ_prop < ring_hom_cring P S Eval
    1.33    apply (unfold Eval_def)
    1.34 -  apply (intro_locales!)
    1.35 +  apply intro_locales
    1.36    apply (rule ring_hom_cring.axioms)
    1.37    apply (rule ring_hom_cring.intro)
    1.38 -  apply intro_locales
    1.39 +  apply unfold_locales
    1.40    apply (rule eval_ring_hom)
    1.41    apply rule
    1.42    done
    1.43 @@ -1276,7 +1276,7 @@
    1.44  proof (rule ring_hom_cring.intro)
    1.45    show "ring_hom_cring_axioms P S Phi"
    1.46    by (rule ring_hom_cring_axioms.intro) (rule Phi)
    1.47 -qed intro_locales
    1.48 +qed unfold_locales
    1.49  
    1.50  theorem (in UP_pre_univ_prop) UP_universal_property:
    1.51    assumes S: "s \<in> carrier S"