Replaced "hand-made" LaTeX code in Protocol/protocol.tex by
generated files in Protocol/document.
--- a/doc-src/TutorialI/Makefile Mon Jul 23 14:34:27 2007 +0200
+++ b/doc-src/TutorialI/Makefile Mon Jul 23 14:36:37 2007 +0200
@@ -20,7 +20,9 @@
Inductive/inductive.tex Inductive/document/AB.tex \
Inductive/document/Advanced.tex Inductive/document/Even.tex \
Inductive/document/Mutual.tex Inductive/document/Star.tex \
- Protocol/protocol.tex \
+ Protocol/protocol.tex Protocol/document/Event.tex \
+ Protocol/document/Message.tex Protocol/document/Public.tex \
+ Protocol/document/NS_Public.tex \
Rules/rules.tex Sets/sets.tex \
Types/numerics.tex Types/types.tex \
Documents/documents.tex \