# HG changeset patch
# User paulson
# Date 982075563 -3600
# Node ID ba314b436aab144678bddb4ae9eeff98b8bd371e
# Parent  f2024fed9f0c8fb64a1a7124ab9f6b0ec3d5f9db
partial conversion to Isar script style in HOL/Auth removes some .ML files

diff -r f2024fed9f0c -r ba314b436aab src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Feb 13 13:16:27 2001 +0100
+++ b/src/HOL/IsaMakefile	Tue Feb 13 15:46:03 2001 +0100
@@ -300,13 +300,13 @@
 
 HOL-Auth: HOL $(LOG)/HOL-Auth.gz
 
-$(LOG)/HOL-Auth.gz: $(OUT)/HOL Auth/Event.ML Auth/Event.thy \
-  Auth/Message.ML Auth/Message.thy Auth/NS_Public.ML Auth/NS_Public.thy \
-  Auth/NS_Public_Bad.ML Auth/NS_Public_Bad.thy Auth/NS_Shared.ML \
+$(LOG)/HOL-Auth.gz: $(OUT)/HOL Auth/Event_lemmas.ML Auth/Event.thy \
+  Auth/Message.ML Auth/Message.thy Auth/NS_Public.thy \
+  Auth/NS_Public_Bad.thy \
   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/OtwayRees_Bad.thy Auth/Public_lemmas.ML Auth/Public.thy Auth/ROOT.ML \
+  Auth/Recur.ML Auth/Recur.thy Auth/Shared_lemmas.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 \