src/HOL/BNF/BNF.thy
author blanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 54006 9fe1bd54d437
parent 53124 9ae9bbaccee1
child 54026 82d9b2701a03
permissions -rw-r--r--
renamed theory file
blanchet@49509
     1
(*  Title:      HOL/BNF/BNF.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@49017
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@49017
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48975
     5
    Copyright   2012
blanchet@48975
     6
blanchet@49509
     7
Bounded natural functors for (co)datatypes.
blanchet@48975
     8
*)
blanchet@48975
     9
blanchet@49509
    10
header {* Bounded Natural Functors for (Co)datatypes *}
blanchet@48975
    11
blanchet@49509
    12
theory BNF
traytel@53124
    13
imports More_BNFs BNF_LFP BNF_GFP
blanchet@48975
    14
begin
blanchet@48975
    15
traytel@52731
    16
hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
traytel@51909
    17
  convol thePull pick_middlep fstOp sndOp csquare inver
traytel@51446
    18
  image2 relImage relInvImage prefCl PrefCl Succ Shift shift
traytel@51446
    19
blanchet@48975
    20
end