diff -r 23a8c5ac35f8 -r 69916a850301 doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -61,8 +61,8 @@
      msg = Agent  agent
          | Nonce  nat
          | Key    key
-	 | MPair  msg msg
-	 | Crypt  key msg
+         | MPair  msg msg
+         | Crypt  key msg
 
 text {*
 \noindent
@@ -855,8 +855,8 @@
     (Fake_insert_simp_tac ss 1
      THEN
      IF_UNSOLVED (Blast.depth_tac
-		  (cs addIs [analz_insertI,
-				   impOfSubs analz_subset_parts]) 4 1))
+                  (cs addIs [analz_insertI,
+                                   impOfSubs analz_subset_parts]) 4 1))
 
 fun spy_analz_tac (cs,ss) i =
   DETERM