--- a/src/HOL/Library/Extended_Reals.thy Wed Jun 01 11:51:25 2011 +0200
+++ b/src/HOL/Library/Extended_Reals.thy Wed Jun 01 13:50:37 2011 +0200
@@ -74,10 +74,10 @@
fixes a :: extreal shows "- (- a) = a"
by (cases a) simp_all
-lemma MInfty_eq[simp]:
+lemma MInfty_eq[simp, code_post]:
"MInfty = - \<infinity>" by simp
-declare uminus_extreal.simps(2)[simp del]
+declare uminus_extreal.simps(2)[code_inline, simp del]
lemma extreal_cases[case_names real PInf MInf, cases type: extreal]:
assumes "\<And>r. x = extreal r \<Longrightarrow> P"