--- a/src/HOL/UNITY/Token.thy Thu Aug 06 14:04:49 1998 +0200 +++ b/src/HOL/UNITY/Token.thy Thu Aug 06 15:47:26 1998 +0200 @@ -9,7 +9,7 @@ *) -Token = WFair + +Token = WFair + (*process states*) datatype pstate = Hungry | Eating | Thinking