src/HOL/IsaMakefile

   $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
   $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
   $(SRC)/Pure/section_utils.ML $(SRC)/TFL/dcterm.sml \
-  $(SRC)/TFL/post.sml $(SRC)/TFL/rules.new.sml $(SRC)/TFL/rules.sig \
+  $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig \
   $(SRC)/TFL/sys.sml $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
   $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
   $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
   $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
   Datatype.thy Divides.ML Divides.thy Finite.ML Finite.thy Fun.ML \

   Auth/NS_Shared.thy Auth/OtwayRees.ML Auth/OtwayRees.thy \
   Auth/OtwayRees_AN.ML Auth/OtwayRees_AN.thy Auth/OtwayRees_Bad.ML \
   Auth/OtwayRees_Bad.thy Auth/Public.ML Auth/Public.thy Auth/ROOT.ML \
   Auth/Recur.ML Auth/Recur.thy Auth/Shared.ML Auth/Shared.thy \
   Auth/TLS.ML Auth/TLS.thy Auth/WooLam.ML Auth/WooLam.thy \
+  Auth/Kerberos_BAN.ML Auth/Kerberos_BAN.thy \
+  Auth/KerberosIV.ML Auth/KerberosIV.thy \
   Auth/Yahalom.ML Auth/Yahalom.thy Auth/Yahalom2.ML Auth/Yahalom2.thy \
   Auth/Yahalom_Bad.ML Auth/Yahalom_Bad.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Auth