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