src/HOL/Enum.thy
changeset 62343 24106dc44def
parent 61799 4cf66f21b764
child 62390 842917225d56
     1.1 --- a/src/HOL/Enum.thy	Wed Feb 17 21:51:55 2016 +0100
     1.2 +++ b/src/HOL/Enum.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -556,7 +556,7 @@
     1.4  end
     1.5  
     1.6  instance finite_1 :: complete_distrib_lattice
     1.7 -by intro_classes(simp_all add: INF_def SUP_def)
     1.8 +  by standard simp_all
     1.9  
    1.10  instance finite_1 :: complete_linorder ..
    1.11  
    1.12 @@ -679,7 +679,7 @@
    1.13  end
    1.14  
    1.15  instance finite_2 :: complete_distrib_lattice
    1.16 -by(intro_classes)(auto simp add: INF_def SUP_def sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def)
    1.17 +  by standard (auto simp add: sup_finite_2_def inf_finite_2_def Inf_finite_2_def Sup_finite_2_def)
    1.18  
    1.19  instance finite_2 :: complete_linorder ..
    1.20  
    1.21 @@ -797,11 +797,11 @@
    1.22      then have "\<And>x. x \<in> B \<Longrightarrow> x = a\<^sub>3"
    1.23        by(case_tac x)(auto simp add: Inf_finite_3_def split: split_if_asm)
    1.24      then show ?thesis using a\<^sub>2_a\<^sub>3
    1.25 -      by(auto simp add: INF_def Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm)
    1.26 -  qed(auto simp add: INF_def Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
    1.27 +      by(auto simp add: Inf_finite_3_def max_def less_eq_finite_3_def less_finite_3_def split: split_if_asm)
    1.28 +  qed (auto simp add: Inf_finite_3_def max_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
    1.29    show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
    1.30 -    by(cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
    1.31 -      (auto simp add: SUP_def Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
    1.32 +    by (cases a "\<Squnion>B" rule: finite_3.exhaust[case_product finite_3.exhaust])
    1.33 +      (auto simp add: Sup_finite_3_def min_def less_finite_3_def less_eq_finite_3_def split: split_if_asm)
    1.34  qed
    1.35  
    1.36  instance finite_3 :: complete_linorder ..
    1.37 @@ -920,10 +920,10 @@
    1.38    fix a :: finite_4 and B
    1.39    show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
    1.40      by(cases a "\<Sqinter>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
    1.41 -      (auto simp add: sup_finite_4_def Inf_finite_4_def INF_def split: finite_4.splits split_if_asm)
    1.42 +      (auto simp add: sup_finite_4_def Inf_finite_4_def split: finite_4.splits split_if_asm)
    1.43    show "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
    1.44      by(cases a "\<Squnion>B" rule: finite_4.exhaust[case_product finite_4.exhaust])
    1.45 -      (auto simp add: inf_finite_4_def Sup_finite_4_def SUP_def split: finite_4.splits split_if_asm)
    1.46 +      (auto simp add: inf_finite_4_def Sup_finite_4_def split: finite_4.splits split_if_asm)
    1.47  qed
    1.48  
    1.49  instantiation finite_4 :: complete_boolean_algebra begin