--- a/src/HOL/Finite_Set.thy Thu Dec 18 15:06:24 2003 +0100
+++ b/src/HOL/Finite_Set.thy Fri Dec 19 04:28:45 2003 +0100
@@ -431,7 +431,9 @@
by (simp add: insert_absorb)
lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
-by (rule_tac t = A in insert_Diff [THEN subst], assumption, simp)
+apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
+apply(simp del:insert_Diff_single)
+done
lemma card_Diff_singleton:
"finite A ==> x: A ==> card (A - {x}) = card A - 1"
@@ -860,7 +862,7 @@
apply (erule ssubst)
apply (drule spec)
apply (erule (1) notE impE)
- apply (simp add: Ball_def)
+ apply (simp add: Ball_def del:insert_Diff_single)
done
subsubsection{* Min and Max of finite linearly ordered sets *}