| changeset 60758 | d8d85a8172b5 |
| parent 58916 | 229765cc3414 |
| child 62905 | 52c5a25e0c96 |
--- a/src/HOL/BNF_Least_Fixpoint.thy Sat Jul 18 21:44:18 2015 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Sat Jul 18 22:58:50 2015 +0200 @@ -7,7 +7,7 @@ Least fixpoint (datatype) operation on bounded natural functors. *) -section {* Least Fixpoint (Datatype) Operation on Bounded Natural Functors *} +section \<open>Least Fixpoint (Datatype) Operation on Bounded Natural Functors\<close> theory BNF_Least_Fixpoint imports BNF_Fixpoint_Base