src/HOL/BNF/BNF.thy
author blanchet
Thu, 16 Jan 2014 21:22:01 +0100
changeset 55024 05cc0dbf3a50
parent 54841 af71b753c459
child 55058 4e700eb471d4
permissions -rw-r--r--
hide short const name

(*  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 proj

end