src/HOL/BNF/BNF.thy
author wenzelm
Fri, 10 Jan 2014 12:05:15 +0100
changeset 54964 bbf2ef613b8c
parent 54841 af71b753c459
child 55024 05cc0dbf3a50
permissions -rw-r--r--
merged

(*  Title:      HOL/BNF/BNF.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Andrei Popescu, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2012

Bounded natural functors for (co)datatypes.
*)

header {* Bounded Natural Functors for (Co)datatypes *}

theory BNF
imports Countable_Set_Type BNF_LFP BNF_GFP BNF_Decl
begin

hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
  prefCl PrefCl Succ Shift shift

end