--- a/src/HOL/UNITY/Detects.thy Thu Jan 30 18:08:09 2003 +0100
+++ b/src/HOL/UNITY/Detects.thy Fri Jan 31 20:12:44 2003 +0100
@@ -6,6 +6,8 @@
Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
*)
+header{*The Detects Relation*}
+
theory Detects = FP + SubstAx:
consts