src/HOL/Enum.thy
changeset 62390 842917225d56
parent 62343 24106dc44def
child 63950 cdc1e59aa513
     1.1 --- a/src/HOL/Enum.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Enum.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -795,13 +795,13 @@
     1.4    proof(cases a "\<Sqinter>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
     1.5      case a\<^sub>2_a\<^sub>3
     1.6      then have "\<And>x. x \<in> B \<Longrightarrow> x = a\<^sub>3"
     1.7 -      by(case_tac x)(auto simp add: Inf_finite_3_def split: split_if_asm)
     1.8 +      by(case_tac x)(auto simp add: Inf_finite_3_def split: if_split_asm)
     1.9      then show ?thesis using a\<^sub>2_a\<^sub>3
    1.10 -      by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm)
    1.11 -  qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
    1.12 +      by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: if_split_asm)
    1.13 +  qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: if_split_asm)
    1.14    show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
    1.15      by (cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
    1.16 -      (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
    1.17 +      (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: if_split_asm)
    1.18  qed
    1.19  
    1.20  instance finite_3 :: complete_linorder ..
    1.21 @@ -920,10 +920,10 @@
    1.22    fix a :: finite_4 and B
    1.23    show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
    1.24      by(cases a "\<Sqinter>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
    1.25 -      (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits split_if_asm)
    1.26 +      (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits if_split_asm)
    1.27    show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
    1.28      by(cases a "\<Squnion>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
    1.29 -      (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits split_if_asm)
    1.30 +      (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits if_split_asm)
    1.31  qed
    1.32  
    1.33  instantiation finite_4 :: complete_boolean_algebra begin
    1.34 @@ -1022,13 +1022,13 @@
    1.35    fix A and z :: finite_5
    1.36    assume *: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
    1.37    show "z \<le> \<Sqinter>A"
    1.38 -    by(auto simp add: less_eq_finite_5_def Inf_finite_5_def split: finite_5.splits split_if_asm dest!: *)
    1.39 +    by(auto simp add: less_eq_finite_5_def Inf_finite_5_def split: finite_5.splits if_split_asm dest!: *)
    1.40  next
    1.41    fix A and z :: finite_5
    1.42    assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
    1.43    show "\<Squnion>A \<le> z"
    1.44 -    by(auto simp add: less_eq_finite_5_def Sup_finite_5_def split: finite_5.splits split_if_asm dest!: *)
    1.45 -qed(auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def Inf_finite_5_def Sup_finite_5_def split: finite_5.splits split_if_asm)
    1.46 +    by(auto simp add: less_eq_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm dest!: *)
    1.47 +qed(auto simp add: less_eq_finite_5_def less_finite_5_def inf_finite_5_def sup_finite_5_def Inf_finite_5_def Sup_finite_5_def split: finite_5.splits if_split_asm)
    1.48  
    1.49  end
    1.50