src/HOL/BNF/BNF.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 54026 82d9b2701a03
child 54539 bbab2ebda234
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
     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 Coinduction
    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