src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 62390 842917225d56
parent 62343 24106dc44def
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -1631,7 +1631,7 @@
     1.4    have "bij_betw F (Pow A) (Func A (UNIV::bool set))"
     1.5    unfolding bij_betw_def inj_on_def proof (intro ballI impI conjI)
     1.6      fix A1 A2 assume "A1 \<in> Pow A" "A2 \<in> Pow A" "F A1 = F A2"
     1.7 -    thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: split_if_asm)
     1.8 +    thus "A1 = A2" unfolding F_def Pow_def fun_eq_iff by (auto split: if_split_asm)
     1.9    next
    1.10      show "F ` Pow A = Func A UNIV"
    1.11      proof safe