src/HOL/Codatatype/BNF_Def.thy
changeset 49283 97809ae5f7bb
parent 49282 c057e1b39f16
child 49284 5f39b7940b49
equal deleted inserted replaced
49282:c057e1b39f16 49283:97809ae5f7bb
    12 keywords
    12 keywords
    13   "print_bnfs" :: diag
    13   "print_bnfs" :: diag
    14 and
    14 and
    15   "bnf_def" :: thy_goal
    15   "bnf_def" :: thy_goal
    16 uses
    16 uses
    17   "Tools/bnf_util.ML"
       
    18   "Tools/bnf_tactics.ML"
       
    19   "Tools/bnf_def.ML"
    17   "Tools/bnf_def.ML"
    20 begin
    18 begin
    21 
    19 
    22 end
    20 end