author | blanchet |
Mon, 20 Jan 2014 18:24:56 +0100 | |
changeset 55058 | 4e700eb471d4 |
parent 55024 | 05cc0dbf3a50 |
child 55069 | b3e44be90122 |
permissions | -rw-r--r-- |
(* 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_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