--- a/src/ZF/UNITY/FP.thy Thu Jul 23 14:20:51 2015 +0200
+++ b/src/ZF/UNITY/FP.thy Thu Jul 23 14:25:05 2015 +0200
@@ -7,7 +7,7 @@
Theory ported from HOL.
*)
-section{*Fixed Point of a Program*}
+section\<open>Fixed Point of a Program\<close>
theory FP imports UNITY begin