diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -30,7 +30,7 @@
 
 rules
     (*The ticket should remain fresh for two journeys on the network at least*)
-    SesKeyLife_LB "# 2 <= SesKeyLife"
+    SesKeyLife_LB "2 <= SesKeyLife"
 
     (*The authenticator only for one journey*)
     AutLife_LB    "Suc 0 <= AutLife"