src/HOL/Codatatype/BNF_FP.thy
author blanchet
Wed Sep 12 05:03:18 2012 +0200 (2012-09-12)
changeset 49308 6190b701e4f4
child 49309 f20b24214ac2
permissions -rw-r--r--
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
blanchet@49308
     1
(*  Title:      HOL/Codatatype/BNF_FP.thy
blanchet@49308
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@49308
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@49308
     4
    Copyright   2012
blanchet@49308
     5
blanchet@49308
     6
Composition of bounded natural functors.
blanchet@49308
     7
*)
blanchet@49308
     8
blanchet@49308
     9
header {* Composition of Bounded Natural Functors *}
blanchet@49308
    10
blanchet@49308
    11
theory BNF_FP
blanchet@49308
    12
imports BNF_Comp BNF_Wrap
blanchet@49308
    13
keywords
blanchet@49308
    14
  "defaults"
blanchet@49308
    15
uses
blanchet@49308
    16
  "Tools/bnf_fp_util.ML"
blanchet@49308
    17
  "Tools/bnf_fp_sugar_tactics.ML"
blanchet@49308
    18
  "Tools/bnf_fp_sugar.ML"
blanchet@49308
    19
begin
blanchet@49308
    20
blanchet@49308
    21
end