changeset 62958 | b41c1cb5e251 |
parent 62597 | b3f2b8c906a6 |
child 63161 | 2660ba498798 |
--- a/src/HOL/Code_Evaluation.thy Tue Apr 12 13:49:37 2016 +0200 +++ b/src/HOL/Code_Evaluation.thy Tue Apr 12 14:38:57 2016 +0200 @@ -69,6 +69,7 @@ subsection \<open>Tools setup and evaluation\<close> lemma eq_eq_TrueD: + fixes x y :: "'a::{}" assumes "(x \<equiv> y) \<equiv> Trueprop True" shows "x \<equiv> y" using assms by simp