# HG changeset patch
# User wenzelm
# Date 1295018091 -3600
# Node ID ccfc070e8157ba1ba0ef331d290d30ec71755223
# Parent  4638b1210d26009490ca30d5750a2d008333650c# Parent  c5e71fee36178267232a9447d360a9e866217218
merged

diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Big_Operators.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -172,7 +172,7 @@
 lemma (in comm_monoid_add) setsum_reindex_cong:
    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
     ==> setsum h B = setsum g A"
-  by (simp add: setsum_reindex cong: setsum_cong)
+  by (simp add: setsum_reindex)
 
 lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0"
   by (cases "finite A") (erule finite_induct, auto)
@@ -288,7 +288,7 @@
   shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
 proof -
   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
-  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint cong: setsum_cong)
+  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint)
 qed
 
 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
@@ -310,7 +310,7 @@
   shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
 proof -
   interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
-  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def cong: setsum_cong)
+  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def)
 qed
 
 text{*Here we can eliminate the finiteness assumptions, by cases.*}
@@ -498,7 +498,7 @@
   assumes "finite A"  "A \<noteq> {}"
     and "!!x. x:A \<Longrightarrow> f x < g x"
   shows "setsum f A < setsum g A"
-  using prems
+  using assms
 proof (induct rule: finite_ne_induct)
   case singleton thus ?case by simp
 next
@@ -775,7 +775,7 @@
 apply (subgoal_tac
          "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
 apply (simp add: setsum_UN_disjoint del: setsum_constant)
-apply (simp cong: setsum_cong)
+apply simp
 done
 
 lemma card_Union_disjoint:
@@ -947,7 +947,7 @@
   let ?f = "(\<lambda>k. if k=a then b k else 1)"
   {assume a: "a \<notin> S"
     hence "\<forall> k\<in> S. ?f k = 1" by simp
-    hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
+    hence ?thesis  using a by (simp add: setprod_1) }
   moreover 
   {assume a: "a \<in> S"
     let ?A = "S - {a}"
@@ -959,7 +959,7 @@
     have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
       using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
       by simp
-    then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
+    then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)}
   ultimately show ?thesis by blast
 qed
 
@@ -975,7 +975,7 @@
     "finite I ==> (ALL i:I. finite (A i)) ==>
         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
-by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
+  by (simp add: setprod_def fold_image_UN_disjoint)
 
 lemma setprod_Union_disjoint:
   "[| (ALL A:C. finite A);
@@ -990,7 +990,7 @@
 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
-by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
+by(simp add:setprod_def fold_image_Sigma split_def)
 
 text{*Here we can eliminate the finiteness assumptions, by cases.*}
 lemma setprod_cartesian_product: 
@@ -1332,7 +1332,7 @@
   shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
 using A proof (induct rule: finite_ne_induct)
   case singleton thus ?case
-    by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
+    by (simp add: sup_Inf1_distrib [OF B])
 next
   interpret ab_semigroup_idem_mult inf
     by (rule ab_semigroup_idem_mult_inf)
@@ -1347,7 +1347,7 @@
   qed
   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
-    using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
+    using insert by simp
   also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
   also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:sup_Inf1_distrib[OF B])
@@ -1391,7 +1391,7 @@
   interpret ab_semigroup_idem_mult sup
     by (rule ab_semigroup_idem_mult_sup)
   have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
-    using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
+    using insert by simp
   also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
   also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
     using insert by(simp add:inf_Sup1_distrib[OF B])
@@ -1551,15 +1551,15 @@
 next
   interpret ab_semigroup_idem_mult min
     by (rule ab_semigroup_idem_mult_min)
-  assume "A \<noteq> B"
+  assume neq: "A \<noteq> B"
   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
   have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
   also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
   proof -
     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
-    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
-    moreover have "(B-A) \<noteq> {}" using prems by blast
-    moreover have "A Int (B-A) = {}" using prems by blast
+    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`])
+    moreover have "(B-A) \<noteq> {}" using assms neq by blast
+    moreover have "A Int (B-A) = {}" using assms by blast
     ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
   qed
   also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Deriv.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -355,7 +355,7 @@
 lemma differentiableE [elim?]:
   assumes "f differentiable x"
   obtains df where "DERIV f x :> df"
-  using prems unfolding differentiable_def ..
+  using assms unfolding differentiable_def ..
 
 lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
 by (simp add: differentiable_def)
@@ -408,7 +408,7 @@
   assumes "f differentiable x"
   assumes "g differentiable x"
   shows "(\<lambda>x. f x - g x) differentiable x"
-  unfolding diff_minus using prems by simp
+  unfolding diff_minus using assms by simp
 
 lemma differentiable_mult [simp]:
   assumes "f differentiable x"
@@ -437,13 +437,16 @@
   assumes "f differentiable x"
   assumes "g differentiable x" and "g x \<noteq> 0"
   shows "(\<lambda>x. f x / g x) differentiable x"
-  unfolding divide_inverse using prems by simp
+  unfolding divide_inverse using assms by simp
 
 lemma differentiable_power [simp]:
   fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
   assumes "f differentiable x"
   shows "(\<lambda>x. f x ^ n) differentiable x"
-  by (induct n, simp, simp add: prems)
+  apply (induct n)
+  apply simp
+  apply (simp add: assms)
+  done
 
 
 subsection {* Nested Intervals and Bisection *}
@@ -1227,7 +1230,7 @@
   assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
   shows "f a < f b"
 proof (rule ccontr)
-  assume "~ f a < f b"
+  assume f: "~ f a < f b"
   have "EX l z. a < z & z < b & DERIV f z :> l
       & f b - f a = (b - a) * l"
     apply (rule MVT)
@@ -1236,13 +1239,12 @@
       apply (metis DERIV_isCont)
      apply (metis differentiableI less_le)
     done
-  then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
+  then obtain l z where z: "a < z" "z < b" "DERIV f z :> l"
       and "f b - f a = (b - a) * l"
     by auto
-  
-  from prems have "~(l > 0)"
+  with assms f have "~(l > 0)"
     by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le)
-  with prems show False
+  with assms z show False
     by (metis DERIV_unique less_le)
 qed
 
@@ -1252,9 +1254,8 @@
     "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<ge> 0)"
   shows "f a \<le> f b"
 proof (rule ccontr, cases "a = b")
-  assume "~ f a \<le> f b"
-  assume "a = b"
-  with prems show False by auto
+  assume "~ f a \<le> f b" and "a = b"
+  then show False by auto
 next
   assume A: "~ f a \<le> f b"
   assume B: "a ~= b"
@@ -1266,13 +1267,13 @@
       apply (metis DERIV_isCont)
      apply (metis differentiableI less_le)
     done
-  then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
+  then obtain l z where z: "a < z" "z < b" "DERIV f z :> l"
       and C: "f b - f a = (b - a) * l"
     by auto
   with A have "a < b" "f b < f a" by auto
   with C have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)
     (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono real_add_left_mono real_le_linear real_le_refl)
-  with prems show False
+  with assms z show False
     by (metis DERIV_unique order_less_imp_le)
 qed
 
@@ -1509,14 +1510,14 @@
 theorem GMVT:
   fixes a b :: real
   assumes alb: "a < b"
-  and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
-  and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
-  and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
-  and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
+    and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
+    and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
+    and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
+    and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
   shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
 proof -
   let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
-  from prems have "a < b" by simp
+  from assms have "a < b" by simp
   moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
   proof -
     have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Divides.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -681,8 +681,8 @@
 ML {*
 local
 
-structure CancelDivMod = CancelDivModFun(struct
-
+structure CancelDivMod = CancelDivModFun
+(
   val div_name = @{const_name div};
   val mod_name = @{const_name mod};
   val mk_binop = HOLogic.mk_binop;
@@ -691,12 +691,9 @@
 
   val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
 
-  val trans = trans;
-
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
     (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
-
-end)
+)
 
 in
 
@@ -1352,15 +1349,16 @@
 theorem posDivAlg_correct:
   assumes "0 \<le> a" and "0 < b"
   shows "divmod_int_rel a b (posDivAlg a b)"
-using prems apply (induct a b rule: posDivAlg.induct)
-apply auto
-apply (simp add: divmod_int_rel_def)
-apply (subst posDivAlg_eqn, simp add: right_distrib)
-apply (case_tac "a < b")
-apply simp_all
-apply (erule splitE)
-apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
-done
+  using assms
+  apply (induct a b rule: posDivAlg.induct)
+  apply auto
+  apply (simp add: divmod_int_rel_def)
+  apply (subst posDivAlg_eqn, simp add: right_distrib)
+  apply (case_tac "a < b")
+  apply simp_all
+  apply (erule splitE)
+  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
+  done
 
 
 subsubsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*}
@@ -1381,15 +1379,16 @@
 lemma negDivAlg_correct:
   assumes "a < 0" and "b > 0"
   shows "divmod_int_rel a b (negDivAlg a b)"
-using prems apply (induct a b rule: negDivAlg.induct)
-apply (auto simp add: linorder_not_le)
-apply (simp add: divmod_int_rel_def)
-apply (subst negDivAlg_eqn, assumption)
-apply (case_tac "a + b < (0\<Colon>int)")
-apply simp_all
-apply (erule splitE)
-apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
-done
+  using assms
+  apply (induct a b rule: negDivAlg.induct)
+  apply (auto simp add: linorder_not_le)
+  apply (simp add: divmod_int_rel_def)
+  apply (subst negDivAlg_eqn, assumption)
+  apply (case_tac "a + b < (0\<Colon>int)")
+  apply simp_all
+  apply (erule splitE)
+  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
+  done
 
 
 subsubsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
@@ -1440,8 +1439,8 @@
 ML {*
 local
 
-structure CancelDivMod = CancelDivModFun(struct
-
+structure CancelDivMod = CancelDivModFun
+(
   val div_name = @{const_name div};
   val mod_name = @{const_name mod};
   val mk_binop = HOLogic.mk_binop;
@@ -1450,12 +1449,9 @@
 
   val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
 
-  val trans = trans;
-
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
     (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
-
-end)
+)
 
 in
 
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Fact.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -12,12 +12,9 @@
 begin
 
 class fact =
-
-fixes 
-  fact :: "'a \<Rightarrow> 'a"
+  fixes fact :: "'a \<Rightarrow> 'a"
 
 instantiation nat :: fact
-
 begin 
 
 fun
@@ -26,7 +23,7 @@
   fact_0_nat: "fact_nat 0 = Suc 0"
 | fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
 
-instance proof qed
+instance ..
 
 end
 
@@ -93,8 +90,7 @@
 lemma fact_plus_one_int: 
   assumes "n >= 0"
   shows "fact ((n::int) + 1) = (n + 1) * fact n"
-
-  using prems unfolding fact_int_def 
+  using assms unfolding fact_int_def 
   by (simp add: nat_add_distrib algebra_simps int_mult)
 
 lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
@@ -102,19 +98,19 @@
   apply (erule ssubst)
   apply (subst fact_Suc)
   apply simp_all
-done
+  done
 
 lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
   apply (subgoal_tac "n = (n - 1) + 1")
   apply (erule ssubst)
   apply (subst fact_plus_one_int)
   apply simp_all
-done
+  done
 
 lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
   apply (induct n)
   apply (auto simp add: fact_plus_one_nat)
-done
+  done
 
 lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
   by (simp add: fact_int_def)
@@ -137,7 +133,7 @@
   apply (erule ssubst)
   apply (subst zle_int)
   apply auto
-done
+  done
 
 lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
   apply (induct n)
@@ -147,7 +143,7 @@
   apply (erule ssubst)
   apply (rule dvd_triv_left)
   apply auto
-done
+  done
 
 lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
   apply (case_tac "1 <= n")
@@ -155,7 +151,7 @@
   apply (auto simp add: fact_plus_one_int)
   apply (subgoal_tac "m = i + 1")
   apply auto
-done
+  done
 
 lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow> 
   {i..j+1} = {i..j} Un {j+1}"
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -803,7 +803,7 @@
 proof -
   interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
   from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
+    (simp_all add: Inf_insert inf_commute fold_fun_comm)
 qed
 
 lemma sup_Sup_fold_sup:
@@ -812,7 +812,7 @@
 proof -
   interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
   from `finite A` show ?thesis by (induct A arbitrary: B)
-    (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
+    (simp_all add: Sup_insert sup_commute fold_fun_comm)
 qed
 
 lemma Inf_fold_inf:
@@ -833,7 +833,7 @@
   interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
   from `finite A` show "?fold = ?inf"
   by (induct A arbitrary: B)
-    (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
+    (simp_all add: INFI_def Inf_insert inf_left_commute)
 qed
 
 lemma sup_SUPR_fold_sup:
@@ -844,7 +844,7 @@
   interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
   from `finite A` show "?fold = ?sup"
   by (induct A arbitrary: B)
-    (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
+    (simp_all add: SUPR_def Sup_insert sup_left_commute)
 qed
 
 lemma INFI_fold_inf:
@@ -1197,19 +1197,19 @@
     by (auto simp add: nonempty_iff)
   show ?thesis
   proof cases
-    assume "a = x"
-    thus ?thesis
+    assume a: "a = x"
+    show ?thesis
     proof cases
       assume "A' = {}"
-      with prems show ?thesis by simp
+      with A' a show ?thesis by simp
     next
       assume "A' \<noteq> {}"
-      with prems show ?thesis
+      with A A' a show ?thesis
         by (simp add: fold1_insert mult_assoc [symmetric])
     qed
   next
     assume "a \<noteq> x"
-    with prems show ?thesis
+    with A A' show ?thesis
       by (simp add: insert_commute fold1_eq_fold)
   qed
 qed
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/GCD.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -36,11 +36,8 @@
 subsection {* GCD and LCM definitions *}
 
 class gcd = zero + one + dvd +
-
-fixes
-  gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
-  lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-
+  fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 begin
 
 abbreviation
@@ -186,7 +183,7 @@
       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   shows "P (lcm x y)"
-by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith)
+  using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
 
 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   by (simp add: lcm_int_def)
@@ -632,13 +629,12 @@
   apply (subgoal_tac "b' = b div gcd a b")
   apply (erule ssubst)
   apply (rule div_gcd_coprime_nat)
-  using prems
-  apply force
+  using z apply force
   apply (subst (1) b)
   using z apply force
   apply (subst (1) a)
   using z apply force
-done
+  done
 
 lemma gcd_coprime_int:
   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
@@ -650,13 +646,12 @@
   apply (subgoal_tac "b' = b div gcd a b")
   apply (erule ssubst)
   apply (rule div_gcd_coprime_int)
-  using prems
-  apply force
+  using z apply force
   apply (subst (1) b)
   using z apply force
   apply (subst (1) a)
   using z apply force
-done
+  done
 
 lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
     shows "coprime d (a * b)"
@@ -1192,13 +1187,13 @@
        by auto
      moreover
      {assume db: "d=b"
-       from prems have ?thesis apply simp
+       with nz H have ?thesis apply simp
          apply (rule exI[where x = b], simp)
          apply (rule exI[where x = b])
         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
     moreover
     {assume db: "d < b"
-        {assume "x=0" hence ?thesis  using prems by simp }
+        {assume "x=0" hence ?thesis using nz H by simp }
         moreover
         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
           from db have "d \<le> b - 1" by simp
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -5,7 +5,7 @@
 header {* Linked Lists by ML references *}
 
 theory Linked_Lists
-imports Imperative_HOL Code_Integer
+imports "../Imperative_HOL" Code_Integer
 begin
 
 section {* Definition of Linked Lists *}
@@ -371,13 +371,12 @@
 assumes "Ref.get h1 p = Node x pn"
 assumes "refs_of' (Ref.set p (Node x r1) h1) p rs"
 obtains r1s where "rs = (p#r1s)" and "refs_of' h1 r1 r1s"
-using assms
 proof -
   from assms refs_of'_distinct[OF assms(2)] have "\<exists> r1s. rs = (p # r1s) \<and> refs_of' h1 r1 r1s"
     apply -
     unfolding refs_of'_def'[of _ p]
     apply (auto, frule refs_of_set_ref2) by (auto dest: Ref.noteq_sym)
-  with prems show thesis by auto
+  with assms that show thesis by auto
 qed
 
 section {* Proving make_llist and traverse correct *}
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Import/HOL4Compat.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -64,10 +64,10 @@
   by simp
 
 lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
-  by simp;
+  by simp
 
 lemma one: "ALL v. v = ()"
-  by simp;
+  by simp
 
 lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
   by simp
@@ -103,7 +103,7 @@
   by (simp add: map_pair_def split_def)
 
 lemma pair_case_def: "split = split"
-  ..;
+  ..
 
 lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
   by auto
@@ -128,12 +128,12 @@
 
 lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)"
 proof safe
-  assume "m < n"
+  assume 1: "m < n"
   def P == "%n. n <= m"
   have "(!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
   proof (auto simp add: P_def)
     assume "n <= m"
-    from prems
+    with 1
     show False
       by auto
   qed
@@ -187,7 +187,7 @@
     show "m < n"
       ..
   qed
-qed;
+qed
 
 definition FUNPOW :: "('a => 'a) => nat => 'a => 'a" where
   "FUNPOW f n == f ^^ n"
@@ -242,10 +242,10 @@
   by auto
 
 lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)"
-  by simp;
+  by simp
 
 lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)"
-  by (auto simp add: dvd_def);
+  by (auto simp add: dvd_def)
 
 lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
   by simp
@@ -263,21 +263,21 @@
            (list_case v f M = list_case v' f' M')"
 proof clarify
   fix M M' v f
-  assume "M' = [] \<longrightarrow> v = v'"
-    and "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
+  assume 1: "M' = [] \<longrightarrow> v = v'"
+    and 2: "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
   show "list_case v f M' = list_case v' f' M'"
   proof (rule List.list.case_cong)
     show "M' = M'"
       ..
   next
     assume "M' = []"
-    with prems
+    with 1 2
     show "v = v'"
       by auto
   next
     fix a0 a1
     assume "M' = a0 # a1"
-    with prems
+    with 1 2
     show "f a0 a1 = f' a0 a1"
       by auto
   qed
@@ -302,14 +302,14 @@
     by auto
 next
   fix fn1 fn2
-  assume "ALL h t. fn1 (h # t) = f (fn1 t) h t"
-  assume "ALL h t. fn2 (h # t) = f (fn2 t) h t"
-  assume "fn2 [] = fn1 []"
+  assume 1: "ALL h t. fn1 (h # t) = f (fn1 t) h t"
+  assume 2: "ALL h t. fn2 (h # t) = f (fn2 t) h t"
+  assume 3: "fn2 [] = fn1 []"
   show "fn1 = fn2"
   proof
     fix xs
     show "fn1 xs = fn2 xs"
-      by (induct xs,simp_all add: prems) 
+      by (induct xs) (simp_all add: 1 2 3) 
   qed
 qed
 
@@ -411,7 +411,7 @@
   by (simp add: Let_def)
 
 lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
-  by simp;
+  by simp
 
 lemma REAL_SUP_ALLPOS: "\<lbrakk> ALL x. P (x::real) \<longrightarrow> 0 < x ; EX x. P x; EX z. ALL x. P x \<longrightarrow> x < z \<rbrakk> \<Longrightarrow> EX s. ALL y. (EX x. P x & y < x) = (y < s)"
 proof safe
@@ -424,12 +424,11 @@
     show "ALL x : Collect P. 0 < x"
     proof safe
       fix x
-      assume "P x"
+      assume P: "P x"
       from allx
       have "P x \<longrightarrow> 0 < x"
         ..
-      thus "0 < x"
-        by (simp add: prems)
+      with P show "0 < x" by simp
     qed
   next
     from px
@@ -461,7 +460,7 @@
   by simp
 
 lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
-  by auto;
+  by auto
 
 lemma [hol4rew]: "real (0::nat) = 0"
   by simp
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Import/HOL4Setup.thy
--- a/src/HOL/Import/HOL4Setup.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Import/HOL4Setup.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -90,11 +90,11 @@
   have ed: "TYPE_DEFINITION P Rep"
   proof (auto simp add: TYPE_DEFINITION)
     fix x y
-    assume "Rep x = Rep y"
+    assume b: "Rep x = Rep y"
     from td have "x = Abs (Rep x)"
       by auto
     also have "Abs (Rep x) = Abs (Rep y)"
-      by (simp add: prems)
+      by (simp add: b)
     also from td have "Abs (Rep y) = y"
       by auto
     finally show "x = y" .
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Lim.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -653,7 +653,7 @@
   moreover have "\<forall>n. ?F n \<noteq> a"
     by (rule allI) (rule F1)
 
-  moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by simp
+  moreover note `\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
   ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
   
   moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Ln.thy
--- a/src/HOL/Ln.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Ln.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -71,7 +71,7 @@
     qed
     moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)"
       apply (simp add: mult_compare_simps)
-      apply (simp add: prems)
+      apply (simp add: assms)
       apply (subgoal_tac "0 <= x * (x * x^n)")
       apply force
       apply (rule mult_nonneg_nonneg, rule a)+
@@ -91,7 +91,7 @@
       by simp
     also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)"
       apply (rule mult_left_mono)
-      apply (rule prems)
+      apply (rule c)
       apply simp
       done
     also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)"
@@ -129,7 +129,7 @@
     have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <=
         suminf (%n. (x^2/2) * ((1/2)^n))"
       apply (rule summable_le)
-      apply (auto simp only: aux1 prems)
+      apply (auto simp only: aux1 a b)
       apply (rule exp_tail_after_first_two_terms_summable)
       by (rule sums_summable, rule aux2)  
     also have "... = x^2"
@@ -155,14 +155,14 @@
     apply (rule divide_left_mono)
     apply (auto simp add: exp_ge_add_one_self_aux)
     apply (rule add_nonneg_nonneg)
-    apply (insert prems, auto)
+    using a apply auto
     apply (rule mult_pos_pos)
     apply auto
     apply (rule add_pos_nonneg)
     apply auto
     done
   also from a have "... <= 1 + x"
-    by(simp add:field_simps zero_compare_simps)
+    by (simp add: field_simps zero_compare_simps)
   finally show ?thesis .
 qed
 
@@ -192,14 +192,14 @@
   finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
   moreover have "0 < 1 + x + x^2"
     apply (rule add_pos_nonneg)
-    apply (insert a, auto)
+    using a apply auto
     done
   ultimately have "1 - x <= 1 / (1 + x + x^2)"
     by (elim mult_imp_le_div_pos)
   also have "... <= 1 / exp x"
     apply (rule divide_left_mono)
     apply (rule exp_bound, rule a)
-    apply (insert prems, auto)
+    using a b apply auto
     apply (rule mult_pos_pos)
     apply (rule add_pos_nonneg)
     apply auto
@@ -256,10 +256,10 @@
   also have "- (x / (1 - x)) = -x / (1 - x)"
     by auto
   finally have d: "- x / (1 - x) <= ln (1 - x)" .
-  have "0 < 1 - x" using prems by simp
+  have "0 < 1 - x" using a b by simp
   hence e: "-x - 2 * x^2 <= - x / (1 - x)"
-    using mult_right_le_one_le[of "x*x" "2*x"] prems
-    by(simp add:field_simps power2_eq_square)
+    using mult_right_le_one_le[of "x*x" "2*x"] a b
+    by (simp add:field_simps power2_eq_square)
   from e d show "- x - 2 * x^2 <= ln (1 - x)"
     by (rule order_trans)
 qed
@@ -292,7 +292,7 @@
     "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2"
 proof -
   assume x: "0 <= x"
-  assume "x <= 1"
+  assume x1: "x <= 1"
   from x have "ln (1 + x) <= x"
     by (rule ln_add_one_self_le_self)
   then have "ln (1 + x) - x <= 0" 
@@ -303,7 +303,7 @@
     by simp
   also have "... <= x^2"
   proof -
-    from prems have "x - x^2 <= ln (1 + x)"
+    from x x1 have "x - x^2 <= ln (1 + x)"
       by (intro ln_one_plus_pos_lower_bound)
     thus ?thesis
       by simp
@@ -314,19 +314,19 @@
 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
     "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2"
 proof -
-  assume "-(1 / 2) <= x"
-  assume "x <= 0"
+  assume a: "-(1 / 2) <= x"
+  assume b: "x <= 0"
   have "abs(ln (1 + x) - x) = x - ln(1 - (-x))" 
     apply (subst abs_of_nonpos)
     apply simp
     apply (rule ln_add_one_self_le_self2)
-    apply (insert prems, auto)
+    using a apply auto
     done
   also have "... <= 2 * x^2"
     apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))")
     apply (simp add: algebra_simps)
     apply (rule ln_one_minus_pos_lower_bound)
-    apply (insert prems, auto)
+    using a b apply auto
     done
   finally show ?thesis .
 qed
@@ -343,9 +343,9 @@
 
 lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
 proof -
-  assume "exp 1 <= x" and "x <= y"
+  assume x: "exp 1 <= x" "x <= y"
   have a: "0 < x" and b: "0 < y"
-    apply (insert prems)
+    apply (insert x)
     apply (subgoal_tac "0 < exp (1::real)")
     apply arith
     apply auto
@@ -361,12 +361,12 @@
     done
   also have "y / x = (x + (y - x)) / x"
     by simp
-  also have "... = 1 + (y - x) / x" using a prems by(simp add:field_simps)
+  also have "... = 1 + (y - x) / x" using x a by (simp add: field_simps)
   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
     apply (rule mult_left_mono)
     apply (rule ln_add_one_self_le_self)
     apply (rule divide_nonneg_pos)
-    apply (insert prems a, simp_all) 
+    using x a apply simp_all
     done
   also have "... = y - x" using a by simp
   also have "... = (y - x) * ln (exp 1)" by simp
@@ -375,16 +375,16 @@
     apply (subst ln_le_cancel_iff)
     apply force
     apply (rule a)
-    apply (rule prems)
-    apply (insert prems, simp)
+    apply (rule x)
+    using x apply simp
     done
   also have "... = y * ln x - x * ln x"
     by (rule left_diff_distrib)
   finally have "x * ln y <= y * ln x"
     by arith
-  then have "ln y <= (y * ln x) / x" using a by(simp add:field_simps)
-  also have "... = y * (ln x / x)"  by simp
-  finally show ?thesis using b by(simp add:field_simps)
+  then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
+  also have "... = y * (ln x / x)" by simp
+  finally show ?thesis using b by (simp add: field_simps)
 qed
 
 end
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Log.thy
--- a/src/HOL/Log.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Log.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -251,10 +251,11 @@
   apply (erule order_less_imp_le)
 done
 
-lemma ln_powr_bound2: "1 < x ==> 0 < a ==> (ln x) powr a <= (a powr a) * x"
+lemma ln_powr_bound2:
+  assumes "1 < x" and "0 < a"
+  shows "(ln x) powr a <= (a powr a) * x"
 proof -
-  assume "1 < x" and "0 < a"
-  then have "ln x <= (x powr (1 / a)) / (1 / a)"
+  from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
     apply (intro ln_powr_bound)
     apply (erule order_less_imp_le)
     apply (rule divide_pos_pos)
@@ -264,14 +265,14 @@
     by simp
   finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
     apply (intro powr_mono2)
-    apply (rule order_less_imp_le, rule prems)
+    apply (rule order_less_imp_le, rule assms)
     apply (rule ln_gt_zero)
-    apply (rule prems)
+    apply (rule assms)
     apply assumption
     done
   also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
     apply (rule powr_mult)
-    apply (rule prems)
+    apply (rule assms)
     apply (rule powr_gt_zero)
     done
   also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
@@ -279,35 +280,37 @@
   also have "... = x"
     apply simp
     apply (subgoal_tac "a ~= 0")
-    apply (insert prems, auto)
+    using assms apply auto
     done
   finally show ?thesis .
 qed
 
-lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0"
+lemma LIMSEQ_neg_powr:
+  assumes s: "0 < s"
+  shows "(%x. (real x) powr - s) ----> 0"
   apply (unfold LIMSEQ_iff)
   apply clarsimp
   apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
   apply clarify
-  proof -
-    fix r fix n
-    assume "0 < s" and "0 < r" and "natfloor (r powr (1 / - s)) + 1 <= n"
-    have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
-      by (rule real_natfloor_add_one_gt)
-    also have "... = real(natfloor(r powr (1 / -s)) + 1)"
-      by simp
-    also have "... <= real n"
-      apply (subst real_of_nat_le_iff)
-      apply (rule prems)
-      done
-    finally have "r powr (1 / - s) < real n".
-    then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
-      apply (intro powr_less_mono2_neg)
-      apply (auto simp add: prems)
-      done
-    also have "... = r"
-      by (simp add: powr_powr prems less_imp_neq [THEN not_sym])
-    finally show "real n powr - s < r" .
-  qed
+proof -
+  fix r fix n
+  assume r: "0 < r" and n: "natfloor (r powr (1 / - s)) + 1 <= n"
+  have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
+    by (rule real_natfloor_add_one_gt)
+  also have "... = real(natfloor(r powr (1 / -s)) + 1)"
+    by simp
+  also have "... <= real n"
+    apply (subst real_of_nat_le_iff)
+    apply (rule n)
+    done
+  finally have "r powr (1 / - s) < real n".
+  then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
+    apply (intro powr_less_mono2_neg)
+    apply (auto simp add: s)
+    done
+  also have "... = r"
+    by (simp add: powr_powr s r less_imp_neq [THEN not_sym])
+  finally show "real n powr - s < r" .
+qed
 
 end
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Map.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -111,7 +111,7 @@
   assumes "m(a\<mapsto>x) = n(a\<mapsto>y)"
   shows "x = y"
 proof -
-  from prems have "(m(a\<mapsto>x)) a = (n(a\<mapsto>y)) a" by simp
+  from assms have "(m(a\<mapsto>x)) a = (n(a\<mapsto>y)) a" by simp
   then show ?thesis by simp
 qed
 
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Matrix/ComputeFloat.thy
--- a/src/HOL/Matrix/ComputeFloat.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Matrix/ComputeFloat.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -57,7 +57,7 @@
     show ?case by simp
   next
     case (Suc m)
-    show ?case by (auto simp add: algebra_simps pow2_add1 prems)
+    show ?case by (auto simp add: algebra_simps pow2_add1 1 Suc)
   qed
 next
   case (2 n)
@@ -88,7 +88,7 @@
       apply (subst pow2_neg[of "int m - a + 1"])
       apply (subst pow2_neg[of "int m + 1"])
       apply auto
-      apply (insert prems)
+      apply (insert Suc)
       apply (auto simp add: algebra_simps)
       done
   qed
@@ -147,8 +147,8 @@
   assumes "real_is_int a" "real_is_int b"
   shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
 proof -
-  from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
-  from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
+  from assms have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
+  from assms have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
   from a obtain a'::int where a':"a = real a'" by auto
   from b obtain b'::int where b':"b = real b'" by auto
   have r: "real a' * real b' = real (a' * b')" by auto
@@ -286,16 +286,16 @@
       show ?case
       proof cases
         assume u: "u \<noteq> 0 \<and> even u"
-        with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
+        with 1 have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
         with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
         then show ?thesis
           apply (subst norm_float.simps)
           apply (simp add: ind)
           done
       next
-        assume "~(u \<noteq> 0 \<and> even u)"
-        then show ?thesis
-          by (simp add: prems float_def)
+        assume nu: "~(u \<noteq> 0 \<and> even u)"
+        show ?thesis
+          by (simp add: nu float_def)
       qed
     qed
   }
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Matrix/LP.thy
--- a/src/HOL/Matrix/LP.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Matrix/LP.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -12,7 +12,7 @@
   "c <= d"    
   shows "a <= b + d"
   apply (rule_tac order_trans[where y = "b+c"])
-  apply (simp_all add: prems)
+  apply (simp_all add: assms)
   done
 
 lemma linprog_dual_estimate:
@@ -26,8 +26,8 @@
   shows
   "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
 proof -
-  from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
-  from prems have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
+  from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
+  from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps)  
   from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
   have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
@@ -44,23 +44,23 @@
   have 11: "abs (c'-c) = abs (c-c')" 
     by (subst 10, subst abs_minus_cancel, simp)
   have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x"
-    by (simp add: 11 prems mult_right_mono)
+    by (simp add: 11 assms mult_right_mono)
   have 13: "(abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x <= (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x"
-    by (simp add: prems mult_right_mono mult_left_mono)  
+    by (simp add: assms mult_right_mono mult_left_mono)  
   have r: "(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x <=  (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"
     apply (rule mult_left_mono)
-    apply (simp add: prems)
+    apply (simp add: assms)
     apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
     apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
     apply (simp_all)
-    apply (rule order_trans[where y="abs (A-A')"], simp_all add: prems)
-    apply (rule order_trans[where y="abs (c-c')"], simp_all add: prems)
+    apply (rule order_trans[where y="abs (A-A')"], simp_all add: assms)
+    apply (rule order_trans[where y="abs (c-c')"], simp_all add: assms)
     done    
   from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"     
     by (simp)
   show ?thesis
     apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
-    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
+    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]])
     done
 qed
 
@@ -73,10 +73,10 @@
   have "0 <= A - A1"    
   proof -
     have 1: "A - A1 = A + (- A1)" by simp
-    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
+    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified assms])
   qed
   then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
-  with prems show "abs (A-A1) <= (A2-A1)" by simp
+  with assms show "abs (A-A1) <= (A2-A1)" by simp
 qed
 
 lemma mult_le_prts:
@@ -95,31 +95,31 @@
   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
     by (simp add: algebra_simps)
   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
-    by (simp_all add: prems mult_mono)
+    by (simp_all add: assms mult_mono)
   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
   proof -
     have "pprt a * nprt b <= pprt a * nprt b2"
-      by (simp add: mult_left_mono prems)
+      by (simp add: mult_left_mono assms)
     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
-      by (simp add: mult_right_mono_neg prems)
+      by (simp add: mult_right_mono_neg assms)
     ultimately show ?thesis
       by simp
   qed
   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
   proof - 
     have "nprt a * pprt b <= nprt a2 * pprt b"
-      by (simp add: mult_right_mono prems)
+      by (simp add: mult_right_mono assms)
     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
-      by (simp add: mult_left_mono_neg prems)
+      by (simp add: mult_left_mono_neg assms)
     ultimately show ?thesis
       by simp
   qed
   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
   proof -
     have "nprt a * nprt b <= nprt a * nprt b1"
-      by (simp add: mult_left_mono_neg prems)
+      by (simp add: mult_left_mono_neg assms)
     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
-      by (simp add: mult_right_mono_neg prems)
+      by (simp add: mult_right_mono_neg assms)
     ultimately show ?thesis
       by simp
   qed
@@ -141,19 +141,19 @@
   "c * x \<le> y * b + (let s1 = c1 - y * A2; s2 = c2 - y * A1 in pprt s2 * pprt r2 + pprt s1 * nprt r2 + nprt s2 * pprt r1 + nprt s1 * nprt r1)"
   (is "_ <= _ + ?C")
 proof -
-  from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
+  from assms have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: algebra_simps)  
   ultimately have "c * x + (y * A - c) * x <= y * b" by simp
   then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
   then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
   have s2: "c - y * A <= c2 - y * A1"
-    by (simp add: diff_minus prems add_mono mult_left_mono)
+    by (simp add: diff_minus assms add_mono mult_left_mono)
   have s1: "c1 - y * A2 <= c - y * A"
-    by (simp add: diff_minus prems add_mono mult_left_mono)
+    by (simp add: diff_minus assms add_mono mult_left_mono)
   have prts: "(c - y * A) * x <= ?C"
     apply (simp add: Let_def)
     apply (rule mult_le_prts)
-    apply (simp_all add: prems s1 s2)
+    apply (simp_all add: assms s1 s2)
     done
   then have "y * b + (c - y * A) * x <= y * b + ?C"
     by simp
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -785,7 +785,7 @@
   hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
   then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force
   then have "c\<notin>A" by simp
-  then show ?thesis using prems by simp 
+  then show ?thesis ..
 qed
 
 text {* there always exists a fresh name for an object with finite support *}
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Power.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -297,7 +297,7 @@
   assume "~ a \<le> b"
   then have "b < a" by (simp only: linorder_not_le)
   then have "b ^ Suc n < a ^ Suc n"
-    by (simp only: prems power_strict_mono)
+    by (simp only: assms power_strict_mono)
   from le and this show False
     by (simp add: linorder_not_less [symmetric])
 qed
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Predicate.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -93,10 +93,10 @@
 subsubsection {* Top and bottom elements *}
 
 lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
-  by (simp add: bot_fun_def bot_bool_def)
+  by (simp add: bot_fun_def)
 
 lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
-  by (simp add: bot_fun_def bot_bool_def)
+  by (simp add: bot_fun_def)
 
 lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
   by (auto simp add: fun_eq_iff)
@@ -105,64 +105,64 @@
   by (auto simp add: fun_eq_iff)
 
 lemma top1I [intro!]: "top x"
-  by (simp add: top_fun_def top_bool_def)
+  by (simp add: top_fun_def)
 
 lemma top2I [intro!]: "top x y"
-  by (simp add: top_fun_def top_bool_def)
+  by (simp add: top_fun_def)
 
 
 subsubsection {* Binary intersection *}
 
 lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
-  by (simp add: inf_fun_def inf_bool_def)
+  by (simp add: inf_fun_def)
 
 lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
-  by (simp add: inf_fun_def inf_bool_def)
+  by (simp add: inf_fun_def)
 
 lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
-  by (simp add: inf_fun_def inf_bool_def)
+  by (simp add: inf_fun_def)
 
 lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
-  by (simp add: inf_fun_def inf_bool_def)
+  by (simp add: inf_fun_def)
 
 lemma inf1D1: "inf A B x ==> A x"
-  by (simp add: inf_fun_def inf_bool_def)
+  by (simp add: inf_fun_def)
 
 lemma inf2D1: "inf A B x y ==> A x y"
-  by (simp add: inf_fun_def inf_bool_def)
+  by (simp add: inf_fun_def)
 
 lemma inf1D2: "inf A B x ==> B x"
-  by (simp add: inf_fun_def inf_bool_def)
+  by (simp add: inf_fun_def)
 
 lemma inf2D2: "inf A B x y ==> B x y"
-  by (simp add: inf_fun_def inf_bool_def)
+  by (simp add: inf_fun_def)
 
 lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
-  by (simp add: inf_fun_def inf_bool_def mem_def)
+  by (simp add: inf_fun_def mem_def)
 
 lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
-  by (simp add: inf_fun_def inf_bool_def mem_def)
+  by (simp add: inf_fun_def mem_def)
 
 
 subsubsection {* Binary union *}
 
 lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
-  by (simp add: sup_fun_def sup_bool_def)
+  by (simp add: sup_fun_def)
 
 lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
-  by (simp add: sup_fun_def sup_bool_def)
+  by (simp add: sup_fun_def)
 
 lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
-  by (simp add: sup_fun_def sup_bool_def)
+  by (simp add: sup_fun_def)
 
 lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
-  by (simp add: sup_fun_def sup_bool_def)
+  by (simp add: sup_fun_def)
 
 lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
-  by (simp add: sup_fun_def sup_bool_def) iprover
+  by (simp add: sup_fun_def) iprover
 
 lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
-  by (simp add: sup_fun_def sup_bool_def) iprover
+  by (simp add: sup_fun_def) iprover
 
 text {*
   \medskip Classical introduction rule: no commitment to @{text A} vs
@@ -170,16 +170,16 @@
 *}
 
 lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
-  by (auto simp add: sup_fun_def sup_bool_def)
+  by (auto simp add: sup_fun_def)
 
 lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
-  by (auto simp add: sup_fun_def sup_bool_def)
+  by (auto simp add: sup_fun_def)
 
 lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
-  by (simp add: sup_fun_def sup_bool_def mem_def)
+  by (simp add: sup_fun_def mem_def)
 
 lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
-  by (simp add: sup_fun_def sup_bool_def mem_def)
+  by (simp add: sup_fun_def mem_def)
 
 
 subsubsection {* Intersections of families *}
@@ -257,7 +257,7 @@
 
 lemma pred_comp_rel_comp_eq [pred_set_conv]:
   "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
-  by (auto simp add: fun_eq_iff elim: pred_compE)
+  by (auto simp add: fun_eq_iff)
 
 
 subsubsection {* Converse *}
@@ -292,12 +292,10 @@
     elim: pred_compE dest: conversepD)
 
 lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
-  by (simp add: inf_fun_def inf_bool_def)
-    (iprover intro: conversepI ext dest: conversepD)
+  by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
 
 lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
-  by (simp add: sup_fun_def sup_bool_def)
-    (iprover intro: conversepI ext dest: conversepD)
+  by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
 
 lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
   by (auto simp add: fun_eq_iff)
@@ -756,7 +754,7 @@
     apply (rule ext)
     apply (simp add: unit_eq)
     done
-  from this prems show ?thesis by blast
+  from this assms show ?thesis by blast
 qed
 
 lemma unit_pred_cases:
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/RComplete.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -517,10 +517,10 @@
   apply simp
 done
 
-lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
-  natfloor (x / real y) = natfloor x div y"
+lemma natfloor_div_nat:
+  assumes "1 <= x" and "y > 0"
+  shows "natfloor (x / real y) = natfloor x div y"
 proof -
-  assume "1 <= (x::real)" and "(y::nat) > 0"
   have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
     by simp
   then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
@@ -535,8 +535,7 @@
     by simp
   also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
     real y + (x - real(natfloor x)) / real y"
-    by (auto simp add: algebra_simps add_divide_distrib
-      diff_divide_distrib prems)
+    by (auto simp add: algebra_simps add_divide_distrib diff_divide_distrib)
   finally have "natfloor (x / real y) = natfloor(...)" by simp
   also have "... = natfloor(real((natfloor x) mod y) /
     real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
@@ -547,11 +546,11 @@
     apply (rule add_nonneg_nonneg)
     apply (rule divide_nonneg_pos)
     apply simp
-    apply (simp add: prems)
+    apply (simp add: assms)
     apply (rule divide_nonneg_pos)
     apply (simp add: algebra_simps)
     apply (rule real_natfloor_le)
-    apply (insert prems, auto)
+    using assms apply auto
     done
   also have "natfloor(real((natfloor x) mod y) /
     real y + (x - real(natfloor x)) / real y) = 0"
@@ -560,13 +559,13 @@
     apply (rule add_nonneg_nonneg)
     apply (rule divide_nonneg_pos)
     apply force
-    apply (force simp add: prems)
+    apply (force simp add: assms)
     apply (rule divide_nonneg_pos)
     apply (simp add: algebra_simps)
     apply (rule real_natfloor_le)
-    apply (auto simp add: prems)
-    apply (insert prems, arith)
-    apply (simp add: add_divide_distrib [THEN sym])
+    apply (auto simp add: assms)
+    using assms apply arith
+    using assms apply (simp add: add_divide_distrib [THEN sym])
     apply (subgoal_tac "real y = real y - 1 + 1")
     apply (erule ssubst)
     apply (rule add_le_less_mono)
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/RealDef.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -1200,7 +1200,7 @@
 lemma real_of_int_div_aux: "d ~= 0 ==> (real (x::int)) / (real d) = 
     real (x div d) + (real (x mod d)) / (real d)"
 proof -
-  assume "d ~= 0"
+  assume d: "d ~= 0"
   have "x = (x div d) * d + x mod d"
     by auto
   then have "real x = real (x div d) * real d + real(x mod d)"
@@ -1208,7 +1208,7 @@
   then have "real x / real d = ... / real d"
     by simp
   then show ?thesis
-    by (auto simp add: add_divide_distrib algebra_simps prems)
+    by (auto simp add: add_divide_distrib algebra_simps d)
 qed
 
 lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
@@ -1353,7 +1353,7 @@
 lemma real_of_nat_div_aux: "0 < d ==> (real (x::nat)) / (real d) = 
     real (x div d) + (real (x mod d)) / (real d)"
 proof -
-  assume "0 < d"
+  assume d: "0 < d"
   have "x = (x div d) * d + x mod d"
     by auto
   then have "real x = real (x div d) * real d + real(x mod d)"
@@ -1361,7 +1361,7 @@
   then have "real x / real d = \<dots> / real d"
     by simp
   then show ?thesis
-    by (auto simp add: add_divide_distrib algebra_simps prems)
+    by (auto simp add: add_divide_distrib algebra_simps d)
 qed
 
 lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==>
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Transcendental.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -164,7 +164,7 @@
   { 
     have "?s 0 = 0" by auto
     have Suc_m1: "\<And> n. Suc n - 1 = n" by auto
-    { fix B T E have "(if \<not> B then T else E) = (if B then E else T)" by auto } note if_eq = this
+    have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto
 
     have "?s sums y" using sums_if'[OF `f sums y`] .
     from this[unfolded sums_def, THEN LIMSEQ_Suc] 
@@ -348,7 +348,7 @@
   fixes z :: "'a :: {monoid_mult,comm_ring}" shows
   "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
    (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
-by(auto simp add: algebra_simps power_add [symmetric] cong: strong_setsum_cong)
+by(auto simp add: algebra_simps power_add [symmetric])
 
 lemma sumr_diff_mult_const2:
   "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)"
@@ -1849,7 +1849,7 @@
 lemma sin_less_zero: 
   assumes lb: "- pi/2 < x" and "x < 0" shows "sin x < 0"
 proof -
-  have "0 < sin (- x)" using prems by (simp only: sin_gt_zero2) 
+  have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2) 
   thus ?thesis by simp
 qed
 
@@ -2107,7 +2107,7 @@
 lemma tan_less_zero: 
   assumes lb: "- pi/2 < x" and "x < 0" shows "tan x < 0"
 proof -
-  have "0 < tan (- x)" using prems by (simp only: tan_gt_zero) 
+  have "0 < tan (- x)" using assms by (simp only: tan_gt_zero) 
   thus ?thesis by simp
 qed
 
diff -r 4638b1210d26 -r ccfc070e8157 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/HOL/Word/Word.thy	Fri Jan 14 16:14:51 2011 +0100
@@ -2171,7 +2171,7 @@
 
 lemma word_of_int_power_hom: 
   "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
-  by (induct n) (simp_all add : word_of_int_hom_syms power_Suc)
+  by (induct n) (simp_all add: word_of_int_hom_syms)
 
 lemma word_arith_power_alt: 
   "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
@@ -2367,7 +2367,7 @@
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
         word_of_int_Ex [where x=z]   
-  by (auto simp: bwsimps bbw_ao_dist simp del: bin_ops_comm)
+  by (auto simp: bwsimps bbw_ao_dist)
 
 lemma word_oa_dist:
   fixes x :: "'a::len0 word"
@@ -2375,7 +2375,7 @@
   using word_of_int_Ex [where x=x] 
         word_of_int_Ex [where x=y] 
         word_of_int_Ex [where x=z]   
-  by (auto simp: bwsimps bbw_oa_dist simp del: bin_ops_comm)
+  by (auto simp: bwsimps bbw_oa_dist)
 
 lemma word_add_not [simp]: 
   fixes x :: "'a::len0 word"
@@ -2571,7 +2571,7 @@
   fixes w :: "'a::len0 word"
   assumes "m ~= n"
   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
-  by (rule word_eqI) (clarsimp simp add : test_bit_set_gen word_size prems)
+  by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
     
 lemma test_bit_no': 
   fixes w :: "'a::len0 word"
@@ -2623,7 +2623,7 @@
   done
 
 lemma word_msb_n1: "msb (-1::'a::len word)"
-  unfolding word_msb_alt word_msb_alt to_bl_n1 by simp
+  unfolding word_msb_alt to_bl_n1 by simp
 
 declare word_set_set_same [simp] word_set_nth [simp]
   test_bit_no [simp] word_set_no [simp] nth_0 [simp]
@@ -3047,7 +3047,7 @@
 
 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
   unfolding shiftl_def 
-  by (induct n) (auto simp: shiftl1_2t power_Suc)
+  by (induct n) (auto simp: shiftl1_2t)
 
 lemma shiftr1_bintr [simp]:
   "(shiftr1 (number_of w) :: 'a :: len0 word) = 
@@ -3940,12 +3940,12 @@
      apply (clarsimp simp: word_size)+
   apply (rule trans)
   apply (rule test_bit_rcat [OF refl refl])
-  apply (simp add : word_size msrevs)
+  apply (simp add: word_size msrevs)
   apply (subst nth_rev)
    apply arith
-  apply (simp add : le0 [THEN [2] xtr7, THEN diff_Suc_less])
+  apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
   apply safe
-  apply (simp add : diff_mult_distrib)
+  apply (simp add: diff_mult_distrib)
   apply (rule mpl_lem)
   apply (cases "size ws")
    apply simp_all
diff -r 4638b1210d26 -r ccfc070e8157 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/Pure/Isar/proof_display.ML	Fri Jan 14 16:14:51 2011 +0100
@@ -80,12 +80,13 @@
 
 local
 
-fun pretty_fact_name (kind, "") = Pretty.str kind
-  | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
-      Pretty.str (Long_Name.base_name name), Pretty.str ":"];
+fun pretty_fact_name (kind, "") = Pretty.command kind
+  | pretty_fact_name (kind, name) =
+      Pretty.block [Pretty.command kind, Pretty.brk 1,
+        Pretty.str (Long_Name.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
-  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
+  flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
     map (single o ProofContext.pretty_fact_aux ctxt false);
 
 in
diff -r 4638b1210d26 -r ccfc070e8157 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Jan 14 16:14:51 2011 +0100
@@ -225,12 +225,12 @@
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
 
-    val {master = (thy_path, _), ...} = deps;
+    val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
     val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
     fun init _ =
-      Thy_Load.begin_theory dir name parent_thys uses
+      Thy_Load.begin_theory dir name imports parent_thys uses
       |> Present.begin_theory update_time dir uses;
 
     val (after_load, theory) = Outer_Syntax.load_thy name init pos text;
@@ -324,7 +324,7 @@
     val _ = kill_thy name;
     val _ = use_thys_wrt dir imports;
     val parent_thys = map (get_theory o base_name) imports;
-  in Thy_Load.begin_theory dir name parent_thys uses end;
+  in Thy_Load.begin_theory dir name imports parent_thys uses end;
 
 
 (* register theory *)
@@ -334,7 +334,8 @@
     val name = Context.theory_name theory;
     val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
     val parents = map Context.theory_name (Theory.parents_of theory);
-    val deps = make_deps master parents;
+    val imports = Thy_Load.imports_of theory;
+    val deps = make_deps master imports;
   in
     NAMED_CRITICAL "Thy_Info" (fn () =>
      (kill_thy name;
diff -r 4638b1210d26 -r ccfc070e8157 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Jan 14 16:14:51 2011 +0100
@@ -13,6 +13,7 @@
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
   val master_directory: theory -> Path.T
+  val imports_of: theory -> string list
   val provide: Path.T * (Path.T * file_ident) -> theory -> theory
   val legacy_show_path: unit -> string list
   val legacy_add_path: string -> unit
@@ -28,7 +29,7 @@
   val provide_file: Path.T -> theory -> theory
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
-  val begin_theory: Path.T -> string -> theory list -> (Path.T * bool) list -> theory
+  val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory
 end;
 
 structure Thy_Load: THY_LOAD =
@@ -83,40 +84,42 @@
 
 type files =
  {master_dir: Path.T,  (*master directory of theory source*)
+  imports: string list,  (*source specification of imports*)
   required: Path.T list,  (*source path*)
   provided: (Path.T * (Path.T * file_ident)) list};  (*source path, physical path, identifier*)
 
-fun make_files (master_dir, required, provided): files =
- {master_dir = master_dir, required = required, provided = provided};
+fun make_files (master_dir, imports, required, provided): files =
+ {master_dir = master_dir, imports = imports, required = required, provided = provided};
 
 structure Files = Theory_Data
 (
   type T = files;
-  val empty = make_files (Path.current, [], []);
+  val empty = make_files (Path.current, [], [], []);
   fun extend _ = empty;
   fun merge _ = empty;
 );
 
 fun map_files f =
-  Files.map (fn {master_dir, required, provided} =>
-    make_files (f (master_dir, required, provided)));
+  Files.map (fn {master_dir, imports, required, provided} =>
+    make_files (f (master_dir, imports, required, provided)));
 
 
 val master_directory = #master_dir o Files.get;
+val imports_of = #imports o Files.get;
 
-fun master dir = map_files (fn _ => (dir, [], []));
+fun put_deps dir imports = map_files (fn _ => (dir, imports, [], []));
 
 fun require src_path =
-  map_files (fn (master_dir, required, provided) =>
+  map_files (fn (master_dir, imports, required, provided) =>
     if member (op =) required src_path then
       error ("Duplicate source file dependency: " ^ Path.implode src_path)
-    else (master_dir, src_path :: required, provided));
+    else (master_dir, imports, src_path :: required, provided));
 
 fun provide (src_path, path_id) =
-  map_files (fn (master_dir, required, provided) =>
+  map_files (fn (master_dir, imports, required, provided) =>
     if AList.defined (op =) provided src_path then
       error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path)
-    else (master_dir, required, (src_path, path_id) :: provided));
+    else (master_dir, imports, required, (src_path, path_id) :: provided));
 
 
 (* maintain default paths *)
@@ -251,9 +254,9 @@
 
 (* begin theory *)
 
-fun begin_theory dir name parents uses =
+fun begin_theory dir name imports parents uses =
   Theory.begin_theory name parents
-  |> master dir
+  |> put_deps dir imports
   |> fold (require o fst) uses
   |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   |> Theory.checkpoint;
diff -r 4638b1210d26 -r ccfc070e8157 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Fri Jan 14 16:00:13 2011 +0100
+++ b/src/Pure/assumption.ML	Fri Jan 14 16:14:51 2011 +0100
@@ -79,10 +79,12 @@
 fun extra_hyps ctxt th =
   subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
 
-(*named prems -- legacy feature*)
 val _ = Context.>>
   (Context.map_theory (Global_Theory.add_thms_dynamic (Binding.name "prems",
-    fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
+    fn Context.Theory _ => []
+     | Context.Proof ctxt =>
+        (legacy_feature ("Use of global prems" ^ Position.str_of (Position.thread_data ()));
+          all_prems_of ctxt))));
 
 
 (* local assumptions *)