changeset 36176 | 3fe7e97ccca8 |
parent 35028 | 108662d50512 |
child 42463 | f270e3e18be5 |
--- a/src/HOL/ex/RPred.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/ex/RPred.thy Fri Apr 16 21:28:09 2010 +0200 @@ -47,6 +47,6 @@ definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a rpred \<Rightarrow> 'b rpred)" where "map f P = bind P (return o f)" -hide (open) const return bind supp map +hide_const (open) return bind supp map end \ No newline at end of file