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