src/HOL/UNITY/Union.thy
changeset 7947 b999c1ab9327
parent 7915 c7fd7eb3b0ef
child 8055 bb15396278fb
equal deleted inserted replaced
7946:95e1de322e82 7947:b999c1ab9327
     6 Unions of programs
     6 Unions of programs
     7 
     7 
     8 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
     8 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
     9 
     9 
    10 Do we need a Meet operator?  (Aka Intersection)
    10 Do we need a Meet operator?  (Aka Intersection)
       
    11 
       
    12 CAN PROBABLY DELETE the "Disjoint" predicate
    11 *)
    13 *)
    12 
    14 
    13 Union = SubstAx + FP +
    15 Union = SubstAx + FP +
    14 
    16 
    15 constdefs
    17 constdefs