author | paulson |
Fri, 21 Jul 2000 18:01:36 +0200 | |
changeset 9403 | aad13b59b8d9 |
parent 8334 | 7896bcbd8641 |
child 13785 | e2fcd88be55d |
permissions | -rw-r--r-- |
(* Title: HOL/UNITY/Detects ID: $Id$ Author: Tanja Vos, Cambridge University Computer Laboratory Copyright 2000 University of Cambridge Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo *) Detects = WFair + Reach + consts op_Detects :: "['a set, 'a set] => 'a program set" (infixl "Detects" 60) op_Equality :: "['a set, 'a set] => 'a set" (infixl "<==>" 60) defs Detects_def "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)" Equality_def "A <==> B == (-A Un B) Int (A Un -B)" end