--- a/doc-src/TutorialI/Protocol/NS_Public.thy Tue Mar 02 17:45:10 2010 +0100
+++ b/doc-src/TutorialI/Protocol/NS_Public.thy Tue Mar 02 17:36:40 2010 +0000
@@ -76,7 +76,7 @@
@{term [display,indent=5] "Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"}
may be extended by an event of the form
@{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"}
-where @{text NB} is a fresh nonce: @{term "Nonce NB \<in> used evs2"}.
+where @{text NB} is a fresh nonce: @{term "Nonce NB \<notin> used evs2"}.
Writing the sender as @{text A'} indicates that @{text B} does not
know who sent the message. Calling the trace variable @{text evs2} rather
than simply @{text evs} helps us know where we are in a proof after many
--- a/doc-src/TutorialI/Protocol/document/NS_Public.tex Tue Mar 02 17:45:10 2010 +0100
+++ b/doc-src/TutorialI/Protocol/document/NS_Public.tex Tue Mar 02 17:36:40 2010 +0000
@@ -84,7 +84,7 @@
\begin{isabelle}%
\ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}%
\end{isabelle}
-where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymin}\ used\ evs{\isadigit{2}}}.
+where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}}.
Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not
know who sent the message. Calling the trace variable \isa{evs{\isadigit{2}}} rather
than simply \isa{evs} helps us know where we are in a proof after many
--- a/src/HOL/List.thy Tue Mar 02 17:45:10 2010 +0100
+++ b/src/HOL/List.thy Tue Mar 02 17:36:40 2010 +0000
@@ -761,13 +761,13 @@
by(induct ys, auto simp add: Cons_eq_map_conv)
lemma map_eq_imp_length_eq:
- assumes "map f xs = map f ys"
+ assumes "map f xs = map g ys"
shows "length xs = length ys"
using assms proof (induct ys arbitrary: xs)
case Nil then show ?case by simp
next
case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
- from Cons xs have "map f zs = map f ys" by simp
+ from Cons xs have "map f zs = map g ys" by simp
moreover with Cons have "length zs = length ys" by blast
with xs show ?case by simp
qed