--- a/doc-src/TutorialI/Protocol/Message_lemmas.ML Wed Jul 11 10:52:20 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML Wed Jul 11 10:53:39 2007 +0200
@@ -450,7 +450,7 @@
\ analz (insert (Crypt K X) H) \\<subseteq> \
\ insert (Crypt K X) (analz (insert X H))";
by (rtac subsetI 1);
-by (eres_inst_tac [("xa","x")] analz.induct 1);
+by (eres_inst_tac [("x","x")] analz.induct 1);
by Auto_tac;
val lemma1 = result();
@@ -458,7 +458,7 @@
\ insert (Crypt K X) (analz (insert X H)) \\<subseteq> \
\ analz (insert (Crypt K X) H)";
by Auto_tac;
-by (eres_inst_tac [("xa","x")] analz.induct 1);
+by (eres_inst_tac [("x","x")] analz.induct 1);
by Auto_tac;
by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
val lemma2 = result();