changeset 60047 | 58e5b16cbd94 |
parent 59975 | da10875adf8e |
child 60054 | ef4878146485 |
--- a/src/HOL/Library/Rewrite.thy Mon Apr 13 00:59:17 2015 +0200 +++ b/src/HOL/Library/Rewrite.thy Mon Apr 13 10:21:35 2015 +0200 @@ -10,7 +10,7 @@ consts rewrite_HOLE :: "'a::{}" notation rewrite_HOLE ("HOLE") -notation rewrite_HOLE ("\<box>") +notation rewrite_HOLE ("\<hole>") lemma eta_expand: fixes f :: "'a::{} \<Rightarrow> 'b::{}"