src/HOL/UNITY/Handshake.thy

--- a/src/HOL/UNITY/Handshake.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Handshake.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -21,14 +21,14 @@
     "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
 
   F :: "state program"
-    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
+    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
 
   (*G's program*)
   cmdG :: "(state*state) set"
     "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
 
   G :: "state program"
-    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
+    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
 
   (*the joint invariant*)
   invFG :: "state set"