--- a/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 14:45:44 2015 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 14:52:40 2015 +0200
@@ -82,6 +82,13 @@
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. \<hole>)" add.commute) fact
+(* This is not limited to the first assumption *)
+lemma
+ assumes "PROP P \<equiv> PROP Q"
+ shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
+ by (rewrite at asm assms)
+
+
(* Rewriting with conditional rewriting rules works just as well. *)
lemma test_theorem: