# HG changeset patch
# User bulwahn
# Date 1306929037 -7200
# Node ID 818521a90356ccaf0d35bcaa7dae577edf07b22f
# Parent  32b888e1a1701a3c074865207d7b9c80887e8600
setting up code generation for extended reals

diff -r 32b888e1a170 -r 818521a90356 src/HOL/Library/Extended_Reals.thy
--- 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"