# HG changeset patch
# User paulson
# Date 924862822 -7200
# Node ID a185927883e525cd17ec2bbd6b15909f118205eb
# Parent  d3b8440e1d472acf66ce9d1e523ae4b610f1c6b4
Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml

diff -r d3b8440e1d47 -r a185927883e5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 23 11:51:38 1999 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 23 12:20:22 1999 +0200
@@ -38,7 +38,7 @@
   $(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 \
@@ -156,6 +156,8 @@
   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