Protocols chapter
authorpaulson
Tue Apr 10 16:11:01 2001 +0200 (2001-04-10)
changeset 11249a0e3c67c1394
parent 11248 7a696a130de2
child 11250 c8bbf4c4bc2d
Protocols chapter
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Protocol/ROOT.ML
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/IsaMakefile	Tue Apr 10 16:09:26 2001 +0200
     1.2 +++ b/doc-src/TutorialI/IsaMakefile	Tue Apr 10 16:11:01 2001 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  ## targets
     1.6  
     1.7 -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
     1.8 +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
     1.9  images:
    1.10  test:
    1.11  all: default
    1.12 @@ -170,7 +170,19 @@
    1.13  	@rm -f tutorial.dvi
    1.14  
    1.15  
    1.16 +## HOL-Protocol
    1.17 +
    1.18 +HOL-Protocol: HOL $(LOG)/HOL-Protocol.gz
    1.19 +
    1.20 +$(LOG)/HOL-Protocol.gz: $(OUT)/HOL Protocol/ROOT.ML  \
    1.21 +  Protocol/Message.thy Protocol/Message_lemmas.ML  \
    1.22 +  Protocol/Event.thy Protocol/Event_lemmas.ML  \
    1.23 +  Protocol/Public.thy Protocol/Public_lemmas.ML \
    1.24 +  Protocol/NS_Public.thy    
    1.25 +	$(USEDIR) Protocol
    1.26 +	@rm -f tutorial.dvi
    1.27 +
    1.28  ## clean
    1.29  
    1.30  clean:
    1.31 -	@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
    1.32 +	@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
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/TutorialI/Protocol/ROOT.ML	Tue Apr 10 16:11:01 2001 +0200
     2.3 @@ -0,0 +1,7 @@
     2.4 +(* ID:         $Id$ 
     2.5 +
     2.6 +To update:
     2.7 +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} .
     2.8 +*)
     2.9 +
    2.10 +use_thy "NS_Public";
     3.1 --- a/doc-src/TutorialI/tutorial.tex	Tue Apr 10 16:09:26 2001 +0200
     3.2 +++ b/doc-src/TutorialI/tutorial.tex	Tue Apr 10 16:11:01 2001 +0200
     3.3 @@ -90,7 +90,7 @@
     3.4  \input{Types/types}
     3.5  \input{Advanced/advanced}
     3.6  %\chapter{Theory Presentation} Document preparation / Syntax Matters!
     3.7 -%\chapter{Case Study: Verifying a Cryptographic Protocol}
     3.8 +\input{Protocol/protocol}
     3.9  %\chapter{Structured Proofs}
    3.10  %\label{ch:Isar}
    3.11  %\chapter{Case Study: UNIX File-System Security}