# HG changeset patch
# User wenzelm
# Date 1329429204 -3600
# Node ID 1b24c24017dd9c9ea64e97f881048c98b4a7e3da
# Parent  c7faa011bfa767ff3ad3366fd22973f57089786c
tuned proofs;

diff -r c7faa011bfa7 -r 1b24c24017dd src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Thu Feb 16 22:18:28 2012 +0100
+++ b/src/HOL/Library/AList.thy	Thu Feb 16 22:53:24 2012 +0100
@@ -135,7 +135,7 @@
 lemma updates_twist [simp]:
  "k \<notin> set ks \<Longrightarrow> 
   map_of (updates ks vs (update k v al)) = map_of (update k v (updates ks vs al))"
-  by (simp add: updates_conv' update_conv' map_upds_twist)
+  by (simp add: updates_conv' update_conv')
 
 lemma updates_apply_notin[simp]:
  "k \<notin> set ks ==> map_of (updates ks vs al) k = map_of al k"
diff -r c7faa011bfa7 -r 1b24c24017dd src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Thu Feb 16 22:18:28 2012 +0100
+++ b/src/HOL/Library/Binomial.thy	Thu Feb 16 22:53:24 2012 +0100
@@ -68,8 +68,7 @@
   need to reason about division.*}
 lemma binomial_Suc_Suc_eq_times:
     "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
-  by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
-    del: mult_Suc mult_Suc_right)
+  by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right)
 
 text{*Another version, with -1 instead of Suc.*}
 lemma times_binomial_minus1_eq:
@@ -255,7 +254,7 @@
 proof-
   from kn obtain h where h: "k = Suc h" by (cases k, auto)
   {assume n0: "n=0" then have ?thesis using kn 
-      by (cases k, simp_all add: pochhammer_rec del: pochhammer_Suc)}
+      by (cases k) (simp_all add: pochhammer_rec)}
   moreover
   {assume n0: "n \<noteq> 0"
     then have ?thesis apply (simp add: h pochhammer_Suc_setprod)
@@ -311,7 +310,7 @@
       using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
       by auto
     have ?thesis
-      unfolding h h pochhammer_Suc_setprod eq setprod_timesf[symmetric]
+      unfolding h pochhammer_Suc_setprod eq setprod_timesf[symmetric]
       apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
       apply (auto simp add: inj_on_def image_def h )
       apply (rule_tac x="h - x" in bexI)
diff -r c7faa011bfa7 -r 1b24c24017dd src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Thu Feb 16 22:18:28 2012 +0100
+++ b/src/HOL/Library/DAList.thy	Thu Feb 16 22:53:24 2012 +0100
@@ -12,8 +12,10 @@
 subsection {* Type @{text "('key, 'value) alist" } *}
 
 typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}"
-morphisms impl_of Alist
-by(rule exI[where x="[]"]) simp
+  morphisms impl_of Alist
+proof
+  show "[] \<in> {xs. distinct (map fst xs)}" by simp
+qed
 
 lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
 by(simp add: impl_of_inject)