src/HOL/UNITY/Simple/NSP_Bad.thy
changeset 42463 f270e3e18be5
parent 37936 1e4c5015a72e
child 42767 e6d920bea7a6
     1.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    Proc. Royal Soc. 426 (1989).
     1.5  *}
     1.6  
     1.7 -types state = "event list"
     1.8 +type_synonym state = "event list"
     1.9  
    1.10    (*The spy MAY say anything he CAN say.  We do not expect him to
    1.11      invent new nonces here, but he can also use NS1.  Common to