| changeset 62390 | 842917225d56 |
| parent 62093 | bd73a2279fcd |
| child 62481 | b5d8e57826df |
--- a/src/HOL/Finite_Set.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Finite_Set.thy Tue Feb 23 16:25:08 2016 +0100 @@ -1312,7 +1312,7 @@ apply (subgoal_tac "finite A & A - {x} <= F") prefer 2 apply (blast intro: finite_subset, atomize) apply (drule_tac x = "A - {x}" in spec) -apply (simp add: card_Diff_singleton_if split add: split_if_asm) +apply (simp add: card_Diff_singleton_if split add: if_split_asm) apply (case_tac "card A", auto) done