diff -r 40efb87985b5 -r 47de509bdd55 src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Thu Jan 09 10:20:03 1997 +0100
+++ b/src/HOL/Auth/Public.thy	Thu Jan 09 10:22:11 1997 +0100
@@ -50,6 +50,13 @@
   sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
 
 
+constdefs
+  (*Set of items that might be visible to somebody: complement of the set
+        of fresh items*)
+  used :: event list => msg set
+    "used evs == parts (UN lost B. sees lost B evs)"
+
+
 (*Agents generate "random" nonces, uniquely determined by their argument.*)
 consts
   newN  :: nat => nat