# HG changeset patch
# User paulson
# Date 983536015 -3600
# Node ID a9d7b050b74af78b9ffe31e31ea48f7744cd65a6
# Parent  44e157622cb28611473776fc0a252e2fe9406457
conversion of Message.thy to Isar format

diff -r 44e157622cb2 -r a9d7b050b74a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 02 13:18:56 2001 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 02 13:26:55 2001 +0100
@@ -301,7 +301,7 @@
 HOL-Auth: HOL $(LOG)/HOL-Auth.gz
 
 $(LOG)/HOL-Auth.gz: $(OUT)/HOL Auth/Event_lemmas.ML Auth/Event.thy \
-  Auth/Message.ML Auth/Message.thy Auth/NS_Public.thy \
+  Auth/Message_lemmas.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 \