src/HOL/BNF/BNF.thy
changeset 52731 dacd47a0633f
parent 52719 480a3479fa47
child 53124 9ae9bbaccee1
equal deleted inserted replaced
52730:6bf02eb4ddf7 52731:dacd47a0633f
    11 
    11 
    12 theory BNF
    12 theory BNF
    13 imports More_BNFs
    13 imports More_BNFs
    14 begin
    14 begin
    15 
    15 
    16 hide_const (open) vimagep Gr Grp collect fsts snds setl setr 
    16 hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
    17   convol thePull pick_middlep fstOp sndOp csquare inver
    17   convol thePull pick_middlep fstOp sndOp csquare inver
    18   image2 relImage relInvImage prefCl PrefCl Succ Shift shift
    18   image2 relImage relInvImage prefCl PrefCl Succ Shift shift
    19 
    19 
    20 end
    20 end