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