extra syntax for JN, making it more like UN
authorpaulson
Thu Aug 26 11:33:24 1999 +0200 (1999-08-26)
changeset 735998a2afab3f86
parent 7358 9e95b846ad42
child 7360 7d3136b9af08
extra syntax for JN, making it more like UN
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/UNITY/Union.thy	Thu Aug 26 11:32:39 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Thu Aug 26 11:33:24 1999 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  Unions of programs
     1.5  
     1.6  Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
     1.7 +
     1.8 +Do we need a Meet operator?  (Aka Intersection)
     1.9  *)
    1.10  
    1.11  Union = SubstAx + FP +
    1.12 @@ -32,9 +34,12 @@
    1.13      "Disjoint F G == Acts F Int Acts G <= {Id}"
    1.14  
    1.15  syntax
    1.16 +  "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)
    1.17    "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
    1.18  
    1.19  translations
    1.20    "JN x:A. B"   == "JOIN A (%x. B)"
    1.21 +  "JN x y. B"   == "JN x. JN y. B"
    1.22 +  "JN x. B"     == "JOIN UNIV (%x. B)"
    1.23  
    1.24  end