changeset 62390 | 842917225d56 |
parent 61585 | a9599d3d7610 |
child 62597 | b3f2b8c906a6 |
--- a/src/HOL/Library/Cardinality.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Library/Cardinality.thy Tue Feb 23 16:25:08 2016 +0100 @@ -495,7 +495,7 @@ with that show ?thesis by (auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] - dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm) + dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm) qed qed }