changeset 2549 | 0c723635b9e6 |
parent 2516 | 4d68fbe6378b |
child 3465 | e85c24717cad |
--- a/src/HOL/Auth/NS_Public_Bad.thy Thu Jan 23 18:10:29 1997 +0100 +++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Jan 23 18:13:07 1997 +0100 @@ -13,8 +13,9 @@ NS_Public_Bad = Public + -consts lost :: agent set (*No need for it to be a variable*) +consts lost :: agent set (*No need for it to be a variable*) ns_public :: event list set + inductive ns_public intrs (*Initial trace is empty*)