# HG changeset patch
# User paulson
# Date 986911861 -7200
# Node ID a0e3c67c139416d59a9a3934e16cab5e87beec70
# Parent  7a696a130de27be61073d473935a99044bd9a11b
Protocols chapter

diff -r 7a696a130de2 -r a0e3c67c1394 doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Tue Apr 10 16:09:26 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Tue Apr 10 16:11:01 2001 +0200
@@ -4,7 +4,7 @@
 
 ## targets
 
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Real-Types HOL-Misc styles
+default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Real-Types HOL-Misc HOL-Protocol styles
 images:
 test:
 all: default
@@ -170,7 +170,19 @@
 	@rm -f tutorial.dvi
 
 
+## HOL-Protocol
+
+HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz
+
+$(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML  \
+  Protocol/Message.thy Protocol/Message_lemmas.ML  \
+  Protocol/Event.thy Protocol/Event_lemmas.ML  \
+  Protocol/Public.thy Protocol/Public_lemmas.ML \
+  Protocol/NS_Public.thy    
+	$(USEDIR) Protocol
+	@rm -f tutorial.dvi
+
 ## clean
 
 clean:
-	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz
+	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz
diff -r 7a696a130de2 -r a0e3c67c1394 doc-src/TutorialI/Protocol/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Protocol/ROOT.ML	Tue Apr 10 16:11:01 2001 +0200
@@ -0,0 +1,7 @@
+(* ID:         $Id$ 
+
+To update:
+cp /home/lcp/isabelle/Repos/HOL/Auth/{Message.thy,Message_lemmas.ML,Event.thy,Event_lemmas.ML,Public.thy,Public_lemmas.ML,NS_Public.thy} .
+*)
+
+use_thy "NS_Public";
diff -r 7a696a130de2 -r a0e3c67c1394 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Tue Apr 10 16:09:26 2001 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Tue Apr 10 16:11:01 2001 +0200
@@ -90,7 +90,7 @@
 \input{Types/types}
 \input{Advanced/advanced}
 %\chapter{Theory Presentation} Document preparation / Syntax Matters!
-%\chapter{Case Study: Verifying a Cryptographic Protocol}
+\input{Protocol/protocol}
 %\chapter{Structured Proofs}
 %\label{ch:Isar}
 %\chapter{Case Study: UNIX File-System Security}