--- 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
--- 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"
--- 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"
--- 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
--- 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)