src/HOL/IsaMakefile

   Library/Univ_Poly.thy \
   List.thy \
   Main.thy \
   Map.thy \
   NatBin.thy \
+  Nat_Int_Bij.thy \
   nat_simprocs.ML \
   Presburger.thy \
   Real/ContNotDenum.thy \
   Real/Lubs.thy \
   Real/PReal.thy \

   Library/Abstract_Rat.thy \
   Library/BigO.thy Library/Ramsey.thy Library/Efficient_Nat.thy		\
   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				\
   Library/Nested_Environment.thy Library/Zorn.thy			\
   Library/Library/ROOT.ML Library/Library/document/root.tex		\

 
 ## HOL-Auth
 
 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	\
   Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy	\
   Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy	\