1.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -39,13 +39,15 @@
     1.4      by blast
     1.5  
     1.6  abbreviation
     1.7 -  CT :: "event list=>nat"
     1.8 +  CT :: "event list=>nat" where
     1.9    "CT == length "
    1.10  
    1.11 -  expiredK :: "[nat, event list] => bool"
    1.12 +abbreviation
    1.13 +  expiredK :: "[nat, event list] => bool" where
    1.14    "expiredK T evs == sesKlife + T < CT evs"
    1.15  
    1.16 -  expiredA :: "[nat, event list] => bool"
    1.17 +abbreviation
    1.18 +  expiredA :: "[nat, event list] => bool" where
    1.19    "expiredA T evs == authlife + T < CT evs"
    1.20  
    1.21