src/HOL/Auth/Kerberos_BAN.thy
changeset 13507 febb8e5d2a9d
parent 11704 3c50a2cd6f00
child 13926 6e62e5357a10
     1.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -89,5 +89,4 @@
     1.4               Expired Ts evso |]
     1.5            ==> Notes Spy {|Number Ts, Key K|} # evso \\<in> kerberos_ban"
     1.6  
     1.7 -
     1.8  end