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)