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