# HG changeset patch
# User paulson
# Date 1267551400 0
# Node ID 99b3fce7e475fcc94f2604962cd803c7f3b0ee92
# Parent  3d105282262ef9023bf588d434d786347d345e2e# Parent  64d2d54cbf03f2491a7389cf38653313d573c268
merged

diff -r 3d105282262e -r 99b3fce7e475 doc-src/TutorialI/Protocol/NS_Public.thy
--- 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
diff -r 3d105282262e -r 99b3fce7e475 doc-src/TutorialI/Protocol/document/NS_Public.tex
--- 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
diff -r 3d105282262e -r 99b3fce7e475 src/HOL/List.thy
--- 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