src/HOL/Auth/Event.thy
changeset 58305 57752a91eec4
parent 53428 3083c611ec40
child 58310 91ea607a34d8
     1.1 --- a/src/HOL/Auth/Event.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  consts  (*Initial states of agents -- parameter of the construction*)
     1.5    initState :: "agent => msg set"
     1.6  
     1.7 -datatype
     1.8 +datatype_new
     1.9    event = Says  agent agent msg
    1.10          | Gets  agent       msg
    1.11          | Notes agent       msg