src/HOL/UNITY/Union.thy
changeset 5259 86d80749453f
parent 5252 1b0f14d11142
child 5313 1861a564d7e2
--- a/src/HOL/UNITY/Union.thy	Wed Aug 05 18:21:09 1998 +0200
+++ b/src/HOL/UNITY/Union.thy	Wed Aug 05 18:21:37 1998 +0200
@@ -12,8 +12,11 @@
 
 constdefs
 
-   Join :: "['a program, 'a program] => 'a program"
+   Join :: ['a program, 'a program] => 'a program
     "Join prgF prgG == (|Init = Init prgF Int Init prgG,
 			 Acts = Acts prgF Un Acts prgG|)"
 
+   Null :: 'a program
+    "Null == (|Init = UNIV, Acts = {id}|)"
+
 end