--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Fri May 09 08:13:37 2014 +0200
@@ -200,8 +200,8 @@
and aval_ivl' = aval'
proof qed (auto simp: iter'_pfp_above)
-value [code] "list_up(AI_ivl' test3_ivl Top)"
-value [code] "list_up(AI_ivl' test4_ivl Top)"
-value [code] "list_up(AI_ivl' test5_ivl Top)"
+value "list_up(AI_ivl' test3_ivl Top)"
+value "list_up(AI_ivl' test4_ivl Top)"
+value "list_up(AI_ivl' test5_ivl Top)"
end