# HG changeset patch
# User paulson
# Date 957446084 -7200
# Node ID 5bd6332640f82c522f938df131e69ec25f342bc4
# Parent  518a5450ab6d62a06c526b1c6d072405274ed749
card_Pow is no longer a default simprule because it uses unary 2

diff -r 518a5450ab6d -r 5bd6332640f8 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Thu May 04 12:29:18 2000 +0200
+++ b/src/HOL/Finite.ML	Thu May 04 15:14:44 2000 +0200
@@ -566,7 +566,6 @@
 by (rewtac inj_on_def);
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "card_Pow";
-Addsimps [card_Pow];
 
 
 (*Relates to equivalence classes.   Based on a theorem of F. Kammueller's.