# HG changeset patch
# User wenzelm
# Date 1473545684 -7200
# Node ID 6a757f36997e245b84119d0076fdfd9d5ebae1a6
# Parent  4aaeb9427c96455b43e56d209585321f0c68fbaa
tuned proofs;

diff -r 4aaeb9427c96 -r 6a757f36997e src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Sun Sep 11 00:14:37 2016 +0200
+++ b/src/HOL/BNF_Def.thy	Sun Sep 11 00:14:44 2016 +0200
@@ -200,7 +200,7 @@
   by (simp add: the_inv_f_f)
 
 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
-  unfolding vimage2p_def by -
+  unfolding vimage2p_def .
 
 lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
   unfolding rel_fun_def vimage2p_def by auto
diff -r 4aaeb9427c96 -r 6a757f36997e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Sep 11 00:14:37 2016 +0200
+++ b/src/HOL/Divides.thy	Sun Sep 11 00:14:44 2016 +0200
@@ -1793,13 +1793,14 @@
     by (rule div_int_unique)
 next
   fix a b c :: int
-  assume "c \<noteq> 0"
-  hence "\<And>q r. divmod_int_rel a b (q, r)
+  assume c: "c \<noteq> 0"
+  have "\<And>q r. divmod_int_rel a b (q, r)
     \<Longrightarrow> divmod_int_rel (c * a) (c * b) (q, c * r)"
     unfolding divmod_int_rel_def
-    by - (rule linorder_cases [of 0 b], auto simp: algebra_simps
+    by (rule linorder_cases [of 0 b])
+      (use c in \<open>auto simp: algebra_simps
       mult_less_0_iff zero_less_mult_iff mult_strict_right_mono
-      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff)
+      mult_strict_right_mono_neg zero_le_mult_iff mult_le_0_iff\<close>)
   hence "divmod_int_rel (c * a) (c * b) (a div b, c * (a mod b))"
     using divmod_int_rel [of a b] .
   thus "(c * a) div (c * b) = a div b"
diff -r 4aaeb9427c96 -r 6a757f36997e src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Sep 11 00:14:37 2016 +0200
+++ b/src/HOL/List.thy	Sun Sep 11 00:14:44 2016 +0200
@@ -4661,8 +4661,7 @@
   from Suc have "k < card A" by simp
   moreover have "finite A" using assms by (simp add: card_ge_0_finite)
   moreover have "finite {xs. ?k_list k xs}"
-    using finite_lists_length_eq[OF \<open>finite A\<close>, of k]
-    by - (rule finite_subset, auto)
+    by (rule finite_subset) (use finite_lists_length_eq[OF \<open>finite A\<close>, of k] in auto)
   moreover have "\<And>i j. i \<noteq> j \<longrightarrow> {i} \<times> (A - set i) \<inter> {j} \<times> (A - set j) = {}"
     by auto
   moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
diff -r 4aaeb9427c96 -r 6a757f36997e src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun Sep 11 00:14:37 2016 +0200
+++ b/src/HOL/Map.thy	Sun Sep 11 00:14:44 2016 +0200
@@ -695,17 +695,23 @@
 by (metis map_add_subsumed1 map_le_iff_map_add_commute)
 
 lemma dom_eq_singleton_conv: "dom f = {x} \<longleftrightarrow> (\<exists>v. f = [x \<mapsto> v])"
-proof(rule iffI)
-  assume "\<exists>v. f = [x \<mapsto> v]"
-  thus "dom f = {x}" by(auto split: if_split_asm)
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?rhs
+  then show ?lhs by (auto split: if_split_asm)
 next
-  assume "dom f = {x}"
-  then obtain v where "f x = Some v" by auto
-  hence "[x \<mapsto> v] \<subseteq>\<^sub>m f" by(auto simp add: map_le_def)
-  moreover have "f \<subseteq>\<^sub>m [x \<mapsto> v]" using \<open>dom f = {x}\<close> \<open>f x = Some v\<close>
-    by(auto simp add: map_le_def)
-  ultimately have "f = [x \<mapsto> v]" by-(rule map_le_antisym)
-  thus "\<exists>v. f = [x \<mapsto> v]" by blast
+  assume ?lhs
+  then obtain v where v: "f x = Some v" by auto
+  show ?rhs
+  proof
+    show "f = [x \<mapsto> v]"
+    proof (rule map_le_antisym)
+      show "[x \<mapsto> v] \<subseteq>\<^sub>m f"
+        using v by (auto simp add: map_le_def)
+      show "f \<subseteq>\<^sub>m [x \<mapsto> v]"
+        using \<open>dom f = {x}\<close> \<open>f x = Some v\<close> by (auto simp add: map_le_def)
+    qed
+  qed
 qed
 
 
diff -r 4aaeb9427c96 -r 6a757f36997e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Sep 11 00:14:37 2016 +0200
+++ b/src/HOL/Transcendental.thy	Sun Sep 11 00:14:44 2016 +0200
@@ -205,7 +205,7 @@
   also have "card {0<..<2*n} \<le> 2*n - 1" by (cases n) simp_all
   also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)"
     using assms by (simp add: algebra_simps)
-  finally have "4 ^ n \<le> (2 * n choose n) * (2 * n)" by - simp_all
+  finally have "4 ^ n \<le> (2 * n choose n) * (2 * n)" by simp_all
   hence "real (4 ^ n) \<le> real ((2 * n choose n) * (2 * n))"
     by (subst of_nat_le_iff)
   with assms show ?thesis by (simp add: field_simps)