src/HOL/Codatatype/BNF_GFP.thy
author blanchet
Wed Sep 12 05:21:47 2012 +0200 (2012-09-12)
changeset 49309 f20b24214ac2
parent 49308 6190b701e4f4
child 49312 c874ff5658dc
permissions -rw-r--r--
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet@48975
     1
(*  Title:      HOL/Codatatype/BNF_GFP.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
Greatest fixed point operation on bounded natural functors.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
blanchet@48975
     9
blanchet@48975
    10
theory BNF_GFP
blanchet@49308
    11
imports BNF_FP
blanchet@48975
    12
keywords
blanchet@49308
    13
  "codata_raw" :: thy_decl and
blanchet@49308
    14
  "codata" :: thy_decl
blanchet@48975
    15
begin
blanchet@48975
    16
blanchet@49309
    17
ML_file "Tools/bnf_gfp_util.ML"
blanchet@49309
    18
ML_file "Tools/bnf_gfp_tactics.ML"
blanchet@49309
    19
ML_file "Tools/bnf_gfp.ML"
blanchet@49309
    20
blanchet@48975
    21
end