--- a/src/HOL/Auth/Kerberos_BAN.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.thy Fri Nov 17 02:20:03 2006 +0100
@@ -39,13 +39,15 @@
by blast
abbreviation
- CT :: "event list=>nat"
+ CT :: "event list=>nat" where
"CT == length "
- expiredK :: "[nat, event list] => bool"
+abbreviation
+ expiredK :: "[nat, event list] => bool" where
"expiredK T evs == sesKlife + T < CT evs"
- expiredA :: "[nat, event list] => bool"
+abbreviation
+ expiredA :: "[nat, event list] => bool" where
"expiredA T evs == authlife + T < CT evs"