| changeset 60770 | 240563fbf41d |
| parent 59788 | 6f7b6adac439 |
| child 61392 | 331be2820f90 |
--- a/src/ZF/UNITY/Follows.thy Thu Jul 23 14:20:51 2015 +0200 +++ b/src/ZF/UNITY/Follows.thy Thu Jul 23 14:25:05 2015 +0200 @@ -5,7 +5,7 @@ Theory ported from HOL. *) -section{*The "Follows" relation of Charpentier and Sivilotte*} +section\<open>The "Follows" relation of Charpentier and Sivilotte\<close> theory Follows imports SubstAx Increasing begin