diff -r 1b0f14d11142 -r 82a5ca6290aa src/HOL/UNITY/Traces.thy
--- a/src/HOL/UNITY/Traces.thy	Wed Aug 05 10:56:58 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy	Wed Aug 05 10:57:25 1998 +0200
@@ -24,11 +24,22 @@
 	   ==> (s', s#evs) : traces Init Acts"
 
 
+record 'a program =
+  Init :: 'a set
+  Acts :: "('a * 'a)set set"
+
+
+consts reachable :: "'a program => 'a set"
+
+inductive "reachable prg"
+  intrs 
+    Init  "s: Init prg ==> s : reachable prg"
+
+    Acts  "[| act: Acts prg;  s : reachable prg;  (s,s'): act |]
+	   ==> s' : reachable prg"
+
 constdefs
-  reachable :: "'a set * ('a * 'a)set set => 'a set"
-  "reachable == %(Init,Acts). {s. EX evs. (s,evs): traces Init Acts}"
-
-  invariant :: "['a set * ('a * 'a)set set, 'a set] => bool"
-  "invariant == %(Init,Acts) A. Init <= A & stable Acts A"
+  invariant :: "['a program, 'a set] => bool"
+  "invariant prg A == (Init prg) <= A & stable (Acts prg) A"
 
 end