src/ZF/Integ/Int.ML
changeset 11321 01cbbf33779b
parent 9909 111ccda5009b
child 11381 4ab3b7b0938f
--- a/src/ZF/Integ/Int.ML	Mon May 21 14:52:04 2001 +0200
+++ b/src/ZF/Integ/Int.ML	Mon May 21 14:52:27 2001 +0200
@@ -77,7 +77,7 @@
 by Auto_tac;
 qed "int_of_type";
 
-AddIffs [int_of_type];
+Addsimps [int_of_type];
 AddTCs  [int_of_type];