src/HOL/Codatatype/BNF_LFP.thy
changeset 49309 f20b24214ac2
parent 49308 6190b701e4f4
child 49312 c874ff5658dc
equal deleted inserted replaced
49308:6190b701e4f4 49309:f20b24214ac2
    10 theory BNF_LFP
    10 theory BNF_LFP
    11 imports BNF_FP
    11 imports BNF_FP
    12 keywords
    12 keywords
    13   "data_raw" :: thy_decl and
    13   "data_raw" :: thy_decl and
    14   "data" :: thy_decl
    14   "data" :: thy_decl
    15 uses
       
    16   "Tools/bnf_lfp_util.ML"
       
    17   "Tools/bnf_lfp_tactics.ML"
       
    18   "Tools/bnf_lfp.ML"
       
    19 begin
    15 begin
    20 
    16 
       
    17 ML_file "Tools/bnf_lfp_util.ML"
       
    18 ML_file "Tools/bnf_lfp_tactics.ML"
       
    19 ML_file "Tools/bnf_lfp.ML"
       
    20 
    21 end
    21 end