--- 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
--- /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";
--- 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}