src/HOL/Lattices_Big.thy
 changeset 63915 bab633745c7f parent 63290 9ac558ab0906 child 65817 8ee1799fb076
```     1.1 --- a/src/HOL/Lattices_Big.thy	Sun Sep 18 17:59:28 2016 +0200
1.2 +++ b/src/HOL/Lattices_Big.thy	Sun Sep 18 20:33:48 2016 +0200
1.3 @@ -522,9 +522,11 @@
1.4    assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b"
1.5    shows "Min (insert a A) = a"
1.6  proof (cases "A = {}")
1.7 -  case True then show ?thesis by simp
1.8 +  case True
1.9 +  then show ?thesis by simp
1.10  next
1.11 -  case False with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
1.12 +  case False
1.13 +  with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
1.14      by simp
1.15    moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp
1.16    ultimately show ?thesis by (simp add: min.absorb1)
1.17 @@ -534,9 +536,11 @@
1.18    assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a"
1.19    shows "Max (insert a A) = a"
1.20  proof (cases "A = {}")
1.21 -  case True then show ?thesis by simp
1.22 +  case True
1.23 +  then show ?thesis by simp
1.24  next
1.25 -  case False with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
1.26 +  case False
1.27 +  with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
1.28      by simp
1.29    moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp
1.30    ultimately show ?thesis by (simp add: max.absorb1)
```