# HG changeset patch
# User wenzelm
# Date 1178837025 -7200
# Node ID 11cc1ccad58e46f48ffef051c67033d1d888c37e
# Parent  f99617e7103f3a2fbf4f1d10e9920f634983c6b0
tuned proofs;

diff -r f99617e7103f -r 11cc1ccad58e src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/FOL/IFOL.thy	Fri May 11 00:43:45 2007 +0200
@@ -676,37 +676,37 @@
 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
 proof
   assume "!!x. P(x)"
-  show "ALL x. P(x)" ..
+  then show "ALL x. P(x)" ..
 next
   assume "ALL x. P(x)"
-  thus "!!x. P(x)" ..
+  then show "!!x. P(x)" ..
 qed
 
 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
 proof
   assume "A ==> B"
-  thus "A --> B" ..
+  then show "A --> B" ..
 next
   assume "A --> B" and A
-  thus B by (rule mp)
+  then show B by (rule mp)
 qed
 
 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
 proof
   assume "x == y"
-  show "x = y" by (unfold prems) (rule refl)
+  show "x = y" unfolding `x == y` by (rule refl)
 next
   assume "x = y"
-  thus "x == y" by (rule eq_reflection)
+  then show "x == y" by (rule eq_reflection)
 qed
 
 lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
 proof
   assume "A == B"
-  show "A <-> B" by (unfold prems) (rule iff_refl)
+  show "A <-> B" unfolding `A == B` by (rule iff_refl)
 next
   assume "A <-> B"
-  thus "A == B" by (rule iff_reflection)
+  then show "A == B" by (rule iff_reflection)
 qed
 
 lemma atomize_conj [atomize]:
diff -r f99617e7103f -r 11cc1ccad58e src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Fri May 11 00:43:45 2007 +0200
@@ -173,7 +173,7 @@
 
 ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
 
-lemma (in ID) th_y: "d == (a = b)" .
+lemma (in ID) th_y: "d == (a = b)" by fact
 
 thm i2.th_y thm i3.th_y
 
diff -r f99617e7103f -r 11cc1ccad58e src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri May 11 00:43:45 2007 +0200
@@ -1229,7 +1229,8 @@
   shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
 proof -
   interpret UP_univ_prop [R S h P s _]
-    by (auto! intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
+    using `UP_pre_univ_prop R S h` P_def R S
+    by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
   from R
   show ?thesis by (rule Eval_monom)
 qed
diff -r f99617e7103f -r 11cc1ccad58e src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri May 11 00:43:45 2007 +0200
@@ -187,11 +187,11 @@
 	  have "f i * g (k-i) = 0"
 	  proof cases
 	    assume "n < i"
-	    show ?thesis by (auto! simp add: ring_simps)
+	    with `bound n f` show ?thesis by (auto simp add: ring_simps)
 	  next
 	    assume "~ (n < i)"
 	    with bound have "m < k-i" by arith
-	    then show ?thesis by (auto! simp add: ring_simps)
+	    with `bound m g` show ?thesis by (auto simp add: ring_simps)
 	  qed
 	}
 	then show "setsum (%i. f i * g (k-i)) {..k} = 0"
diff -r f99617e7103f -r 11cc1ccad58e src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri May 11 00:43:45 2007 +0200
@@ -266,6 +266,6 @@
     qed
     finally show ?thesis .
   qed
-qed (simp_all! add: continuous_def)
+qed (insert `continuous V norm f`, simp_all add: continuous_def)
 
 end
diff -r f99617e7103f -r 11cc1ccad58e src/HOL/ZF/Zet.thy
--- a/src/HOL/ZF/Zet.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/HOL/ZF/Zet.thy	Fri May 11 00:43:45 2007 +0200
@@ -53,7 +53,7 @@
   shows "Inv A g (g x) \<in> A"
   apply (simp add: Inv_def)
   apply (rule someI2)
-  apply (auto!)
+  using `x \<in> A` apply auto
   done
 
 lemma zet_image_mem:
diff -r f99617e7103f -r 11cc1ccad58e src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Thu May 10 22:11:38 2007 +0200
+++ b/src/ZF/ex/Group.thy	Fri May 11 00:43:45 2007 +0200
@@ -64,13 +64,13 @@
   by (simp add: update_carrier_def)
 
 lemma carrier_update_carrier [simp]: "carrier(update_carrier(M,B)) = B"
-by (simp add: update_carrier_def) 
+  by (simp add: update_carrier_def) 
 
 lemma mult_update_carrier [simp]: "mmult(update_carrier(M,B),x,y) = mmult(M,x,y)"
-by (simp add: update_carrier_def mmult_def) 
+  by (simp add: update_carrier_def mmult_def) 
 
 lemma one_update_carrier [simp]: "one(update_carrier(M,B)) = one(M)"
-by (simp add: update_carrier_def one_def) 
+  by (simp add: update_carrier_def one_def) 
 
 
 lemma (in monoid) inv_unique:
@@ -92,7 +92,7 @@
   assumes inv_ex:
      "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
 
-lemma (in group) is_group [simp]: "group(G)" .
+lemma (in group) is_group [simp]: "group(G)" by fact
 
 theorem groupI:
   includes struct G
@@ -308,7 +308,7 @@
 lemma DirProdGroup_group:
   includes group G + group H
   shows "group (G \<Otimes> H)"
-by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
+  by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
           simp add: DirProdGroup_def)
 
 lemma carrier_DirProdGroup [simp]:
@@ -322,7 +322,7 @@
 lemma mult_DirProdGroup [simp]:
      "[|g \<in> carrier(G); h \<in> carrier(H); g' \<in> carrier(G); h' \<in> carrier(H)|]
       ==> <g, h> \<cdot>\<^bsub>G \<Otimes> H\<^esub> <g', h'> = <g \<cdot>\<^bsub>G\<^esub> g', h \<cdot>\<^bsub>H\<^esub> h'>"
-by (simp add: DirProdGroup_def)
+  by (simp add: DirProdGroup_def)
 
 lemma inv_DirProdGroup [simp]:
   includes group G + group H
@@ -366,7 +366,7 @@
   "G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
 
 lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"
-by (simp add: iso_def hom_def id_type id_bij) 
+  by (simp add: iso_def hom_def id_type id_bij) 
 
 
 lemma (in group) iso_sym:
@@ -380,18 +380,18 @@
 
 lemma (in group) iso_trans: 
      "\<lbrakk>h \<in> G \<cong> H; i \<in> H \<cong> I\<rbrakk> \<Longrightarrow> i O h \<in> G \<cong> I"
-by (auto simp add: iso_def hom_compose comp_bij)
+  by (auto simp add: iso_def hom_compose comp_bij)
 
 lemma DirProdGroup_commute_iso:
   includes group G + group H
   shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
-by (auto simp add: iso_def hom_def inj_def surj_def bij_def) 
+  by (auto simp add: iso_def hom_def inj_def surj_def bij_def) 
 
 lemma DirProdGroup_assoc_iso:
   includes group G + group H + group I
   shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
           \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
-by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) 
+  by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) 
 
 text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   @term{H}, with a homomorphism @{term h} between them*}
@@ -1003,7 +1003,7 @@
   shows "H \<in> rcosets H"
 proof -
   have "H #> \<one> = H"
-    by (rule coset_join2, auto)
+    using _ `subgroup(H, G)` by (rule coset_join2) simp_all
   then show ?thesis
     by (auto simp add: RCOSETS_def intro: sym)
 qed