changeset 39566 | 87a5704673f0 |
parent 39471 | 55e0ff582fa4 |
child 39715 | 9094200d7988 |
child 39719 | b876d7525e72 |
--- a/src/HOL/HOL.thy Mon Sep 20 15:25:32 2010 +0200 +++ b/src/HOL/HOL.thy Mon Sep 20 18:43:18 2010 +0200 @@ -742,7 +742,7 @@ then show False by (rule notE) qed -lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" +lemma atomize_eq [atomize, code]: "(x == y) == Trueprop (x = y)" proof assume "x == y" show "x = y" by (unfold `x == y`) (rule refl)