src/HOL/Finite_Set.thy
changeset 14331 8dbbb7cf3637
parent 14302 6c24235e8d5d
child 14430 5cb24165a2e1
--- a/src/HOL/Finite_Set.thy	Thu Dec 25 23:18:04 2003 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Dec 27 21:02:14 2003 +0100
@@ -483,7 +483,7 @@
     "finite A ==> B <= A ==> card A - card B = card (A - B)"
   apply (subgoal_tac "(A - B) Un B = A")
    prefer 2 apply blast
-  apply (rule add_right_cancel [THEN iffD1])
+  apply (rule nat_add_right_cancel [THEN iffD1])
   apply (rule card_Un_disjoint [THEN subst])
      apply (erule_tac [4] ssubst)
      prefer 3 apply blast