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