src/HOL/UNITY/Detects.thy
changeset 13798 4c1a53627500
parent 13785 e2fcd88be55d
child 13805 3786b2fd6808
     1.1 --- a/src/HOL/UNITY/Detects.thy	Thu Jan 30 18:08:09 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Detects.thy	Fri Jan 31 20:12:44 2003 +0100
     1.3 @@ -6,6 +6,8 @@
     1.4  Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
     1.5  *)
     1.6  
     1.7 +header{*The Detects Relation*}
     1.8 +
     1.9  theory Detects = FP + SubstAx:
    1.10  
    1.11  consts