changeset 49399 | a9d9f3483b71 |
parent 49396 | 73fb17ed2e08 |
child 49496 | 2694d1615eef |
--- a/src/HOL/IMP/Abs_Int3.thy Sun Sep 16 20:16:28 2012 +0200 +++ b/src/HOL/IMP/Abs_Int3.thy Mon Sep 17 02:25:38 2012 +0200 @@ -383,7 +383,7 @@ subsubsection "Tests" -(* FIXME dirty trick to get around some problem with the code generator *) +(* Trick to make the code generator happy. *) lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y" by(rule refl)