changeset 60758 | d8d85a8172b5 |
parent 59726 | 64c2bb331035 |
child 61032 | b57df8eecad6 |
--- a/src/HOL/BNF_Def.thy Sat Jul 18 21:44:18 2015 +0200 +++ b/src/HOL/BNF_Def.thy Sat Jul 18 22:58:50 2015 +0200 @@ -6,7 +6,7 @@ Definition of bounded natural functors. *) -section {* Definition of Bounded Natural Functors *} +section \<open>Definition of Bounded Natural Functors\<close> theory BNF_Def imports BNF_Cardinal_Arithmetic Fun_Def_Base