src/HOL/BNF/BNF.thy
author blanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 54006 9fe1bd54d437
parent 53124 9ae9bbaccee1
child 54026 82d9b2701a03
permissions -rw-r--r--
renamed theory file
     1 (*  Title:      HOL/BNF/BNF.thy
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Andrei Popescu, TU Muenchen
     4     Author:     Jasmin Blanchette, TU Muenchen
     5     Copyright   2012
     6 
     7 Bounded natural functors for (co)datatypes.
     8 *)
     9 
    10 header {* Bounded Natural Functors for (Co)datatypes *}
    11 
    12 theory BNF
    13 imports More_BNFs BNF_LFP BNF_GFP
    14 begin
    15 
    16 hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
    17   convol thePull pick_middlep fstOp sndOp csquare inver
    18   image2 relImage relInvImage prefCl PrefCl Succ Shift shift
    19 
    20 end