changeset 58249 | 180f1b3508ed |
parent 46912 | e0cd5c4df8e6 |
child 58310 | 91ea607a34d8 |
--- a/src/HOL/UNITY/Simple/Token.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/UNITY/Simple/Token.thy Tue Sep 09 20:51:36 2014 +0200 @@ -15,7 +15,7 @@ subsection{*Definitions*} -datatype pstate = Hungry | Eating | Thinking +datatype_new pstate = Hungry | Eating | Thinking --{*process states*} record state =