# HG changeset patch
# User paulson
# Date 845023974 -7200
# Node ID 644104f85d14eac94f49c138fa9c134639da3c51
# Parent  307ebbbec86258b05df25d17c947aed1df2618e4
Addition of OtwayRees_AN

diff -r 307ebbbec862 -r 644104f85d14 src/HOL/Auth/Makefile
--- a/src/HOL/Auth/Makefile	Thu Oct 10 18:40:34 1996 +0200
+++ b/src/HOL/Auth/Makefile	Fri Oct 11 10:52:54 1996 +0200
@@ -4,7 +4,7 @@
 #
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
-NAMES = Message Shared
+NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN Yahalom
 
 FILES = DB-ROOT.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
 
diff -r 307ebbbec862 -r 644104f85d14 src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/ROOT.ML	Thu Oct 10 18:40:34 1996 +0200
+++ b/src/HOL/Auth/ROOT.ML	Fri Oct 11 10:52:54 1996 +0200
@@ -14,5 +14,6 @@
 use_thy "Shared";
 use_thy "NS_Shared";
 use_thy "OtwayRees";
+use_thy "OtwayRees_AN";
 use_thy "Yahalom";
 
diff -r 307ebbbec862 -r 644104f85d14 src/HOL/Makefile
--- a/src/HOL/Makefile	Thu Oct 10 18:40:34 1996 +0200
+++ b/src/HOL/Makefile	Fri Oct 11 10:52:54 1996 +0200
@@ -134,7 +134,7 @@
 
 
 ##Authentication & Security Protocols
-Auth_NAMES = Message Shared NS_Shared OtwayRees
+Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN Yahalom
 
 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)