| changeset 67408 | 4a4c14b24800 |
| parent 67091 | 1393c2340eec |
| child 67452 | aab817885622 |
--- a/src/HOL/Library/Extended_Real.thy Fri Jan 12 14:43:06 2018 +0100 +++ b/src/HOL/Library/Extended_Real.thy Fri Jan 12 15:27:46 2018 +0100 @@ -4091,7 +4091,7 @@ subsubsection \<open>Tests for code generator\<close> -(* A small list of simple arithmetic expressions *) +text \<open>A small list of simple arithmetic expressions.\<close> value "- \<infinity> :: ereal" value "\<bar>-\<infinity>\<bar> :: ereal"