Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
card_Pow is no longer a default simprule because it uses unary 2
authorpaulson
Thu, 04 May 2000 15:14:44 +0200
changeset 8789 5bd6332640f8
parent 8788 518a5450ab6d
child 8790 c4aaa5936e0c
card_Pow is no longer a default simprule because it uses unary 2
src/HOL/Finite.ML file | annotate | diff | comparison | revisions 
--- 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.
isabelle