--- a/src/HOL/Auth/Event.ML Thu Jul 30 23:14:41 1998 +0200
+++ b/src/HOL/Auth/Event.ML Fri Jul 31 10:48:42 1998 +0200
@@ -8,8 +8,6 @@
Datatype of events; function "sees"; freshness
*)
-open Event;
-
AddIffs [Spy_in_bad, Server_not_bad];
(**** Function "spies" ****)