# HG changeset patch
# User paulson
# Date 935660004 -7200
# Node ID 98a2afab3f86d018d632036441a1e896a17a6c30
# Parent  9e95b846ad42e3f3cadcf4d0e90e30489061d0de
extra syntax for JN, making it more like UN

diff -r 9e95b846ad42 -r 98a2afab3f86 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Thu Aug 26 11:32:39 1999 +0200
+++ b/src/HOL/UNITY/Union.thy	Thu Aug 26 11:33:24 1999 +0200
@@ -6,6 +6,8 @@
 Unions of programs
 
 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
+
+Do we need a Meet operator?  (Aka Intersection)
 *)
 
 Union = SubstAx + FP +
@@ -32,9 +34,12 @@
     "Disjoint F G == Acts F Int Acts G <= {Id}"
 
 syntax
+  "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)
   "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
 
 translations
   "JN x:A. B"   == "JOIN A (%x. B)"
+  "JN x y. B"   == "JN x. JN y. B"
+  "JN x. B"     == "JOIN UNIV (%x. B)"
 
 end