# HG changeset patch
# User noschinl
# Date 1428913295 -7200
# Node ID 58e5b16cbd9450aeb26bcaa48924805c4b8fbce4
# Parent  7ff7fdfbb9a079134c21fbdff96d3b7824b554d4
enable \<hole> syntax for rewrite

diff -r 7ff7fdfbb9a0 -r 58e5b16cbd94 src/HOL/Library/Rewrite.thy
--- 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::{}"
diff -r 7ff7fdfbb9a0 -r 58e5b16cbd94 src/HOL/ex/Rewrite_Examples.thy
--- a/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 00:59:17 2015 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 10:21:35 2015 +0200
@@ -22,30 +22,30 @@
   fixes a b c :: int
   assumes "f (a - a + (a - a)) + f (   0    + c) = f 0 + f c"
   shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
-  by (rewrite in "f _ + f \<box> = _" diff_self) fact
+  by (rewrite in "f _ + f \<hole> = _" diff_self) fact
 
 lemma
   fixes a b c :: int
   assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
   shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
-  by (rewrite at "f (_ + \<box>) + f _ = _" diff_self) fact
+  by (rewrite at "f (_ + \<hole>) + f _ = _" diff_self) fact
 
 lemma
   fixes a b c :: int
   assumes "f (  0   + (a - a)) + f ((a - a) + c) = f 0 + f c"
   shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
-  by (rewrite in "f (\<box> + _) + _ = _" diff_self) fact
+  by (rewrite in "f (\<hole> + _) + _ = _" diff_self) fact
 
 lemma
   fixes a b c :: int
   assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
   shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
-  by (rewrite in "f (_ + \<box>) + _ = _" diff_self) fact
+  by (rewrite in "f (_ + \<hole>) + _ = _" diff_self) fact
 
 lemma
   fixes x y :: nat
   shows"x + y > c \<Longrightarrow> y + x > c"
-  by (rewrite at "\<box> > c" add.commute) assumption
+  by (rewrite at "\<hole> > c" add.commute) assumption
 
 (* We can also rewrite in the assumptions.  *)
 lemma
@@ -64,23 +64,23 @@
   fixes x y :: nat
   assumes "y + x > c \<Longrightarrow> y + x > c"
   shows   "x + y > c \<Longrightarrow> y + x > c"
-  by (rewrite at "\<box> > c" at asm  add.commute) fact
+  by (rewrite at "\<hole> > c" at asm  add.commute) fact
 
 lemma
   assumes "P {x::int. y + 1 = 1 + x}"
   shows   "P {x::int. y + 1 = x + 1}"
-  by (rewrite at "x+1" in "{x::int. \<box> }" add.commute) fact
+  by (rewrite at "x+1" in "{x::int. \<hole> }" add.commute) fact
 
 lemma
   assumes "P {x::int. y + 1 = 1 + x}"
   shows   "P {x::int. y + 1 = x + 1}"
-  by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<box> }" add.commute)
+  by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<hole> }" add.commute)
    fact
 
 lemma
   assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}"
   shows   "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
-  by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<box>)" add.commute) fact
+  by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact
 
 
 (* Rewriting with conditional rewriting rules works just as well. *)
@@ -126,13 +126,13 @@
 lemma
   assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
   shows "P (\<lambda>n. f n + 1) = x"
-  by (rewrite in "\<lambda>n. \<box>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
+  by (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
 
 (* Any identifier will work *)
 lemma
   assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
   shows "P (\<lambda>n. f n + 1) = x"
-  by (rewrite in "\<lambda>abc. \<box>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
+  by (rewrite in "\<lambda>abc. \<hole>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
 
 (* The "for" keyword. *)
 lemma
@@ -158,7 +158,7 @@
 lemma
   assumes "\<And>x y z. x + y + z = y + z + (x::int)"
   shows   "\<And>x y z. x + y + z = z + y + (x::int)"
-by (rewrite at "\<box> + _" at "_ = \<box>" in concl at for () add.commute) fact
+by (rewrite at "\<hole> + _" at "_ = \<hole>" in concl at for () add.commute) fact
 
 (* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
 lemma