| changeset 63146 | f1ecba0272f9 |
| parent 61635 | c657ee4f59b7 |
| child 80914 | d97fdabd9e2b |
--- a/src/HOL/UNITY/Detects.thy Wed May 25 11:49:40 2016 +0200 +++ b/src/HOL/UNITY/Detects.thy Wed May 25 11:50:58 2016 +0200 @@ -5,7 +5,7 @@ Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo *) -section{*The Detects Relation*} +section\<open>The Detects Relation\<close> theory Detects imports FP SubstAx begin