src/HOL/BNF/BNF.thy
author blanchet
Thu Jan 16 21:22:01 2014 +0100 (2014-01-16)
changeset 55024 05cc0dbf3a50
parent 54841 af71b753c459
child 55058 4e700eb471d4
permissions -rw-r--r--
hide short const name
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@54601
    13
imports Countable_Set_Type BNF_LFP BNF_GFP BNF_Decl
blanchet@48975
    14
begin
blanchet@48975
    15
traytel@52731
    16
hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
traytel@54841
    17
  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
blanchet@55024
    18
  prefCl PrefCl Succ Shift shift proj
traytel@51446
    19
blanchet@48975
    20
end