1.1 --- a/src/HOL/Auth/KerberosIV.thy	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/Auth/KerberosIV.thy	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -65,8 +65,8 @@
     1.4      RespLife   :: nat 
     1.5  
     1.6  rules
     1.7 -     AuthLife_LB    "# 2 <= AuthLife"
     1.8 -     ServLife_LB    "# 2 <= ServLife"
     1.9 +     AuthLife_LB    "2 <= AuthLife"
    1.10 +     ServLife_LB    "2 <= ServLife"
    1.11       AutcLife_LB    "Suc 0 <= AutcLife" 
    1.12       RespLife_LB    "Suc 0 <= RespLife"
    1.13