# HG changeset patch
# User paulson
# Date 1059063797 -7200
# Node ID 4d682b249437dc4f0b6de41b7094701d73d34e8b
# Parent  a4fc8b1af5e7473ac774ec3bd699273146e13ac6
new theory Library/NatPair

diff -r a4fc8b1af5e7 -r 4d682b249437 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jul 24 18:23:00 2003 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 24 18:23:17 2003 +0200
@@ -197,7 +197,7 @@
 
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
   Library/FuncSet.thy Library/Library.thy \
-  Library/List_Prefix.thy Library/Multiset.thy \
+  Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
   Library/Permutation.thy Library/Primes.thy \
   Library/Quotient.thy Library/Ring_and_Field.thy \
   Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
@@ -354,7 +354,7 @@
 
 HOL-Auth: HOL $(LOG)/HOL-Auth.gz
 
-$(LOG)/HOL-Auth.gz: $(OUT)/HOL \
+$(LOG)/HOL-Auth.gz: $(OUT)/HOL Library/NatPair.thy \
   Auth/CertifiedEmail.thy Auth/Event.thy \
   Auth/Message.thy Auth/NS_Public.thy Auth/NS_Public_Bad.thy \
   Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayRees_AN.thy \