src/HOL/Auth/Yahalom2.thy
changeset 32960 69916a850301
parent 23746 a455e69c31cc
child 37936 1e4c5015a72e
--- a/src/HOL/Auth/Yahalom2.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -51,7 +51,7 @@
            Both agents are quoted in the 2nd certificate to prevent attacks!*)
  | YM3:  "[| evs3 \<in> yahalom;  Key KAB \<notin> used evs3;
              Gets Server {|Agent B, Nonce NB,
-			   Crypt (shrK B) {|Agent A, Nonce NA|}|}
+                           Crypt (shrK B) {|Agent A, Nonce NA|}|}
                \<in> set evs3 |]
           ==> Says Server A
                {|Nonce NB,