--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Fri Nov 17 02:20:03 2006 +0100
@@ -40,13 +40,15 @@
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"