src/HOL/Auth/Recur.thy

--- a/src/HOL/Auth/Recur.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Auth/Recur.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -101,7 +101,7 @@
      etc.
 
    Oops:  "[| evso \<in> recur;  Says Server B RB \<in> set evso;
-	      RB \<in> responses evs';  Key K \<in> parts {RB} |]
+              RB \<in> responses evs';  Key K \<in> parts {RB} |]
            ==> Notes Spy {|Key K, RB|} # evso \<in> recur"
   *)
 
@@ -140,10 +140,10 @@
 apply (rule_tac [2] 
           recur.Nil
            [THEN recur.RA1 [of _ NA], 
-	    THEN recur.RA2 [of _ NB],
-	    THEN recur.RA3 [OF _ _ respond.One 
+            THEN recur.RA2 [of _ NB],
+            THEN recur.RA3 [OF _ _ respond.One 
                                      [THEN respond.Cons [of _ _ K _ K']]],
-	    THEN recur.RA4], possibility)
+            THEN recur.RA4], possibility)
 apply (auto simp add: used_Cons)
 done
 
@@ -241,7 +241,7 @@
                    (K \<in> KK | Key K \<in> analz (insert RB H))"
 apply (erule responses.induct)
 apply (simp_all del: image_insert
-	        add: analz_image_freshK_simps, auto)
+                add: analz_image_freshK_simps, auto)
 done