src/HOL/Library/Library.thy
changeset 15324 c27165172e30
parent 15140 322485b816ac
child 15470 7e12ad2f6672
--- a/src/HOL/Library/Library.thy	Wed Nov 24 10:29:44 2004 +0100
+++ b/src/HOL/Library/Library.thy	Wed Nov 24 10:30:19 2004 +0100
@@ -3,6 +3,7 @@
 imports
   Accessible_Part
   Continuity
+  EfficientNat
   FuncSet
   List_Prefix
   Multiset