Tuned interpretation proofs.

--- a/src/HOL/Algebra/UnivPoly.thy	Thu Feb 11 21:00:36 2010 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon Feb 15 01:27:06 2010 +0100
@@ -1342,14 +1342,8 @@
 text {* Interpretation of ring homomorphism lemmas. *}
 
 sublocale UP_univ_prop < ring_hom_cring P S Eval
-  apply (unfold Eval_def)
-  apply intro_locales
-  apply (rule ring_hom_cring.axioms)
-  apply (rule ring_hom_cring.intro)
-  apply unfold_locales
-  apply (rule eval_ring_hom)
-  apply rule
-  done
+  unfolding Eval_def
+  by unfold_locales (fast intro: eval_ring_hom)
 
 lemma (in UP_cring) monom_pow:
   assumes R: "a \<in> carrier R"
@@ -1436,10 +1430,7 @@
 lemma ring_homD:
   assumes Phi: "Phi \<in> ring_hom P S"
   shows "ring_hom_cring P S Phi"
-proof (rule ring_hom_cring.intro)
-  show "ring_hom_cring_axioms P S Phi"
-  by (rule ring_hom_cring_axioms.intro) (rule Phi)
-qed unfold_locales
+  by unfold_locales (rule Phi)
 
 theorem UP_universal_property:
   assumes S: "s \<in> carrier S"
@@ -1759,9 +1750,9 @@
   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 proof qed simp
+  interpret UP_pre_univ_prop R R id by unfold_locales 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)
+  interpret ring_hom_cring P R "eval R R id a" by unfold_locales (rule eval_ring_hom)
   have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
     and mon0_closed: "monom P a 0 \<in> carrier P" 
     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"

--- a/src/HOL/Lattices.thy	Thu Feb 11 21:00:36 2010 +0100
+++ b/src/HOL/Lattices.thy	Mon Feb 15 01:27:06 2010 +0100
@@ -301,8 +301,7 @@
 
 lemma dual_bounded_lattice:
   "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
-  by (rule bounded_lattice.intro, rule dual_lattice)
-    (unfold_locales, auto simp add: less_le_not_le)
+  by unfold_locales (auto simp add: less_le_not_le)
 
 lemma inf_bot_left [simp]:
   "\<bottom> \<sqinter> x = \<bottom>"