src/HOL/Auth/KerberosIV.thy
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"