src/HOL/IsaMakefile

--- a/src/HOL/IsaMakefile	Wed Feb 01 12:23:14 2006 +0100
+++ b/src/HOL/IsaMakefile	Wed Feb 01 15:22:02 2006 +0100
@@ -398,10 +398,11 @@
 $(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 \
+  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 Auth/KerberosIV.thy \
+  Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy Auth/Kerberos_BAN_Gets.thy \
+  Auth/KerberosIV.thy Auth/KerberosIV_Gets.thy Auth/KerberosV.thy \
   Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
   Auth/ZhouGollmann.thy \
   Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
@@ -410,6 +411,8 @@
   Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \
   Auth/Guard/P1.thy Auth/Guard/P2.thy \
   Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy\
+  Auth/Smartcard/EventSC.thy Auth/Smartcard/ShoupRubinBella.thy\
+  Auth/Smartcard/ShoupRubin.thy Auth/Smartcard/Smartcard.thy\
   Auth/document/root.tex 
 	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth