src/HOL/Code_Evaluation.thy

--- a/src/HOL/Code_Evaluation.thy	Mon Sep 20 18:43:18 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Mon Sep 20 18:43:23 2010 +0200
@@ -62,6 +62,11 @@
 
 subsection {* Tools setup and evaluation *}
 
+lemma eq_eq_TrueD:
+  assumes "(x \<equiv> y) \<equiv> Trueprop True"
+  shows "x \<equiv> y"
+  using assms by simp
+
 use "Tools/code_evaluation.ML"
 
 code_reserved Eval Code_Evaluation