src/HOL/UNITY/Common.thy
changeset 5648 fe887910e32e
parent 5313 1861a564d7e2
child 7537 875754b599df
--- a/src/HOL/UNITY/Common.thy	Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Common.thy	Thu Oct 15 11:35:07 1998 +0200
@@ -10,7 +10,7 @@
 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
 *)
 
-Common = SubstAx +
+Common = SubstAx + Union + 
 
 consts
   ftime,gtime :: nat=>nat