src/HOL/UNITY/Simple/Token.thy

--- a/src/HOL/UNITY/Simple/Token.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/UNITY/Simple/Token.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/UNITY/Token
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 *)
@@ -24,17 +23,16 @@
   proc  :: "nat => pstate"
 
 
-constdefs
-  HasTok :: "nat => state set"
+definition HasTok :: "nat => state set" where
     "HasTok i == {s. token s = i}"
 
-  H :: "nat => state set"
+definition H :: "nat => state set" where
     "H i == {s. proc s i = Hungry}"
 
-  E :: "nat => state set"
+definition E :: "nat => state set" where
     "E i == {s. proc s i = Eating}"
 
-  T :: "nat => state set"
+definition T :: "nat => state set" where
     "T i == {s. proc s i = Thinking}"