src/HOL/Auth/KerberosIV.thy
changeset 11704 3c50a2cd6f00
parent 11701 3d51fbf81c17
child 13507 febb8e5d2a9d
--- a/src/HOL/Auth/KerberosIV.thy	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Auth/KerberosIV.thy	Sat Oct 06 00:02:46 2001 +0200
@@ -65,8 +65,8 @@
     RespLife   :: nat 
 
 rules
-     AuthLife_LB    "# 2 <= AuthLife"
-     ServLife_LB    "# 2 <= ServLife"
+     AuthLife_LB    "2 <= AuthLife"
+     ServLife_LB    "2 <= ServLife"
      AutcLife_LB    "Suc 0 <= AutcLife" 
      RespLife_LB    "Suc 0 <= RespLife"