src/HOL/Finite_Set.thy
changeset 14302 6c24235e8d5d
parent 14208 144f45277d5a
child 14331 8dbbb7cf3637
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Dec 18 15:06:24 2003 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Dec 19 04:28:45 2003 +0100
     1.3 @@ -431,7 +431,9 @@
     1.4    by (simp add: insert_absorb)
     1.5  
     1.6  lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
     1.7 -by (rule_tac t = A in insert_Diff [THEN subst], assumption, simp)
     1.8 +apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
     1.9 +apply(simp del:insert_Diff_single)
    1.10 +done
    1.11  
    1.12  lemma card_Diff_singleton:
    1.13      "finite A ==> x: A ==> card (A - {x}) = card A - 1"
    1.14 @@ -860,7 +862,7 @@
    1.15    apply (erule ssubst)
    1.16    apply (drule spec)
    1.17    apply (erule (1) notE impE)
    1.18 -  apply (simp add: Ball_def)
    1.19 +  apply (simp add: Ball_def del:insert_Diff_single)
    1.20    done
    1.21  
    1.22  subsubsection{* Min and Max of finite linearly ordered sets *}