changeset 11465 | 45d156ede468 |
parent 11185 | 1b737b4c2108 |
child 11701 | 3d51fbf81c17 |
--- a/src/HOL/Auth/KerberosIV.thy Mon Aug 06 13:43:24 2001 +0200 +++ b/src/HOL/Auth/KerberosIV.thy Mon Aug 06 15:46:20 2001 +0200 @@ -65,10 +65,10 @@ RespLife :: nat rules - AuthLife_LB "2 <= AuthLife" - ServLife_LB "2 <= ServLife" - AutcLife_LB "1 <= AutcLife" - RespLife_LB "1 <= RespLife" + AuthLife_LB "#2 <= AuthLife" + ServLife_LB "#2 <= ServLife" + AutcLife_LB "1' <= AutcLife" + RespLife_LB "1' <= RespLife" translations "CT" == "length"