# HG changeset patch
# User berghofe
# Date 1101288489 -3600
# Node ID c93e6fd5db594150ae8b531c813be5fc8cdd0305
# Parent  694f9d3ce90d8b4ddd7a4b625036e55c226c9593
Added Library/EfficientNat

diff -r 694f9d3ce90d -r c93e6fd5db59 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Nov 24 10:27:24 2004 +0100
+++ b/src/HOL/IsaMakefile	Wed Nov 24 10:28:09 2004 +0100
@@ -177,7 +177,7 @@
 HOL-Library: HOL $(LOG)/HOL-Library.gz
 
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
-  Library/FuncSet.thy Library/Library.thy \
+  Library/EfficientNat.thy Library/FuncSet.thy Library/Library.thy \
   Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
   Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
   Library/Nat_Infinity.thy Library/Word.thy Library/word_setup.ML \