--- a/src/HOL/Library/Extended_Real.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri May 09 08:13:37 2014 +0200
@@ -2444,10 +2444,10 @@
(* A small list of simple arithmetic expressions *)
-value [code] "- \<infinity> :: ereal"
-value [code] "\<bar>-\<infinity>\<bar> :: ereal"
-value [code] "4 + 5 / 4 - ereal 2 :: ereal"
-value [code] "ereal 3 < \<infinity>"
-value [code] "real (\<infinity>::ereal) = 0"
+value "- \<infinity> :: ereal"
+value "\<bar>-\<infinity>\<bar> :: ereal"
+value "4 + 5 / 4 - ereal 2 :: ereal"
+value "ereal 3 < \<infinity>"
+value "real (\<infinity>::ereal) = 0"
end