src/HOL/IsaMakefile
changeset 28098 c92850d2d16c
parent 28054 2b84d34c5d02
child 28109 3f76ae637f71
--- a/src/HOL/IsaMakefile	Tue Sep 02 22:20:27 2008 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 02 22:37:20 2008 +0200
@@ -215,6 +215,7 @@
   Main.thy \
   Map.thy \
   NatBin.thy \
+  Nat_Int_Bij.thy \
   nat_simprocs.ML \
   Presburger.thy \
   Real/ContNotDenum.thy \
@@ -288,7 +289,7 @@
   Library/Executable_Set.thy Library/Infinite_Set.thy			\
   Library/FuncSet.thy			\
   Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
-  Library/Multiset.thy Library/NatPair.thy Library/Permutation.thy	\
+  Library/Multiset.thy Library/Permutation.thy	\
   Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
   Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy	\
   Library/README.html Library/Continuity.thy				\
@@ -530,7 +531,7 @@
 
 HOL-Auth: HOL $(LOG)/HOL-Auth.gz
 
-$(LOG)/HOL-Auth.gz: $(OUT)/HOL Library/NatPair.thy			\
+$(LOG)/HOL-Auth.gz: $(OUT)/HOL 						\
   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/OtwayReesBella.thy Auth/OtwayRees_AN.thy	\