src/HOL/BNF_Greatest_Fixpoint.thy
changeset 58352 37745650a3f4
parent 58128 43a1ba26a8cb
child 58826 2ed2eaabe3df
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Sep 16 19:23:37 2014 +0200
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Tue Sep 16 19:23:37 2014 +0200
     1.3 @@ -4,10 +4,10 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5      Copyright   2012, 2013, 2014
     1.6  
     1.7 -Greatest fixed point operation on bounded natural functors.
     1.8 +Greatest fixpoint (codatatype) operation on bounded natural functors.
     1.9  *)
    1.10  
    1.11 -header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
    1.12 +header {* Greatest Fixpoint (Codatatype) Operation on Bounded Natural Functors *}
    1.13  
    1.14  theory BNF_Greatest_Fixpoint
    1.15  imports BNF_Fixpoint_Base String