src/HOL/Transfer.thy

--- a/src/HOL/Transfer.thy	Mon Jun 10 08:39:48 2013 -0400
+++ b/src/HOL/Transfer.thy	Mon Jun 10 06:08:12 2013 -0700
@@ -96,6 +96,9 @@
 lemma transfer_prover_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
   by simp
 
+lemma untransfer_start: "\<lbrakk>Q; Rel (op =) P Q\<rbrakk> \<Longrightarrow> P"
+  unfolding Rel_def by simp
+
 lemma Rel_eq_refl: "Rel (op =) x x"
   unfolding Rel_def ..