Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TLA/Memory/MemClerk.thy
changeset 9517 f58863b1406a
parent 6255 db63752140c7
child 11703 6e5de8d4290a
equal deleted inserted replaced
9516:72b5d28aae58 9517:f58863b1406a 
    60                          & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
 
    60                          & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
 
    61                          & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
 
    61                          & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
 
    62                          & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
 
    62                          & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
 
    63 
    63 
    64   MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
 
    64   MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
 
    65       "MClkISpec send rcv cst == TEMP (!p. MClkIPSpec send rcv cst p)"
 
    65       "MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
 
    66 
    66 
    67 end
 
    67 end
 
    68 
    68 
    69 
    69
isabelle