| changeset 54841 | af71b753c459 |
| parent 54601 | 91a1e4aa7c80 |
| child 55024 | 05cc0dbf3a50 |
--- a/src/HOL/BNF/BNF.thy Fri Dec 20 21:09:01 2013 +0100 +++ b/src/HOL/BNF/BNF.thy Wed Dec 18 11:03:40 2013 +0100 @@ -14,7 +14,7 @@ begin hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr - convol thePull pick_middlep fstOp sndOp csquare inver - image2 relImage relInvImage prefCl PrefCl Succ Shift shift + convol pick_middlep fstOp sndOp csquare inver relImage relInvImage + prefCl PrefCl Succ Shift shift end