# HG changeset patch
# User berghofe
# Date 1101288619 -3600
# Node ID c27165172e3052c4ce2d62126f3ecf5fb4b308cc
# Parent  6c10fe1c0e177320356242a3019f08a0de92070c
Added EfficientNat

diff -r 6c10fe1c0e17 -r c27165172e30 src/HOL/Library/Library.thy
--- 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