src/HOL/Auth/NS_Shared.thy
changeset 2378 fc103154ad8f
parent 2284 80ebd1a213fd
child 2451 ce85a2aafc7a
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Dec 13 10:57:50 1996 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Dec 13 11:00:44 1996 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  NS_Shared = Shared + 
     1.6  
     1.7 -consts  ns_shared   :: "agent set => event list set"
     1.8 +consts  ns_shared   :: agent set => event list set
     1.9  inductive "ns_shared lost"
    1.10    intrs 
    1.11           (*Initial trace is empty*)