--- a/src/HOL/Auth/Kerberos_BAN.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Thu Sep 28 23:42:35 2006 +0200
@@ -20,11 +20,6 @@
(* Temporal model of accidents: session keys can be leaked
ONLY when they have expired *)
-syntax
- CT :: "event list=>nat"
- expiredK :: "[nat, event list] => bool"
- expiredA :: "[nat, event list] => bool"
-
consts
(*Duration of the session key*)
@@ -43,13 +38,15 @@
authlife_LB [iff]: "0 < authlife"
by blast
-
-translations
- "CT" == "length "
+abbreviation
+ CT :: "event list=>nat"
+ "CT == length "
- "expiredK T evs" == "sesKlife + T < CT evs"
+ expiredK :: "[nat, event list] => bool"
+ "expiredK T evs == sesKlife + T < CT evs"
- "expiredA T evs" == "authlife + T < CT evs"
+ expiredA :: "[nat, event list] => bool"
+ "expiredA T evs == authlife + T < CT evs"
constdefs