author | traytel |
Mon, 15 Jul 2013 15:50:39 +0200 | |
changeset 52660 | 7f7311d04727 |
parent 51909 | eb3169abcbd5 |
child 52719 | 480a3479fa47 |
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 More_BNFs begin hide_const (open) Gr Grp collect fsts snds setl setr convol thePull pick_middlep fstOp sndOp csquare inver image2 relImage relInvImage prefCl PrefCl Succ Shift shift end