src/HOL/Codatatype/BNF_LFP.thy
changeset 48975 7f79f94a432c
child 49074 d8af889dcbe3
equal deleted inserted replaced
48974:8882fc8005ad 48975:7f79f94a432c
       
     1 (*  Title:      HOL/Codatatype/BNF_LFP.thy
       
     2     Author:     Dmitriy Traytel, TU Muenchen
       
     3     Copyright   2012
       
     4 
       
     5 Least fixed point operation on bounded natural functors.
       
     6 *)
       
     7 
       
     8 header {* Least Fixed Point Operation on Bounded Natural Functors *}
       
     9 
       
    10 theory BNF_LFP
       
    11 imports BNF_Comp
       
    12 keywords
       
    13   "bnf_data" :: thy_decl
       
    14 uses
       
    15   "Tools/bnf_lfp_util.ML"
       
    16   "Tools/bnf_lfp_tactics.ML"
       
    17   "Tools/bnf_lfp.ML"
       
    18 begin
       
    19 
       
    20 end