diff -r c48050d6928d -r 1894bfc4aee9 src/HOL/UNITY/Traces.thy
--- a/src/HOL/UNITY/Traces.thy	Wed Dec 02 16:14:09 1998 +0100
+++ b/src/HOL/UNITY/Traces.thy	Thu Dec 03 10:45:06 1998 +0100
@@ -25,17 +25,32 @@
 
 
 typedef (Program)
-  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
+  'a program = "{(states :: 'a set,
+		  init   :: 'a set,
+		  acts   :: ('a * 'a)set set).
+		 init <= states &
+		 acts <= Pow(states Times states) &
+		 diag states : acts}"
 
 constdefs
-    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
-    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
+  restrict_rel :: "['a set, ('a * 'a) set] => ('a * 'a) set"
+    "restrict_rel A r == (A Times A) Int r"
 
-    Init :: "'a program => 'a set"
-    "Init F == fst (Rep_Program F)"
+  mk_program :: "('a set * 'a set * ('a * 'a)set set) => 'a program"
+    "mk_program ==
+       %(states, init, acts).
+	Abs_Program (states,
+		     states Int init,
+		     restrict_rel states `` (insert Id acts))"
 
-    Acts :: "'a program => ('a * 'a)set set"
-    "Acts F == snd (Rep_Program F)"
+  States :: "'a program => 'a set"
+    "States F == (%(states, init, acts). states) (Rep_Program F)"
+
+  Init :: "'a program => 'a set"
+    "Init F == (%(states, init, acts). init) (Rep_Program F)"
+
+  Acts :: "'a program => ('a * 'a)set set"
+    "Acts F == (%(states, init, acts). acts) (Rep_Program F)"
 
 
 consts reachable :: "'a program => 'a set"