| changeset 69593 | 3dda49e08b9d |
| parent 69064 | 5840724b1d71 |
| child 70347 | e5cd5471c18a |
--- a/src/HOL/Library/Float.thy Fri Jan 04 21:49:06 2019 +0100 +++ b/src/HOL/Library/Float.thy Fri Jan 04 23:22:53 2019 +0100 @@ -639,7 +639,7 @@ end -subsection \<open>Lemmas for types @{typ real}, @{typ nat}, @{typ int}\<close> +subsection \<open>Lemmas for types \<^typ>\<open>real\<close>, \<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>\<close> lemmas real_of_ints = of_int_add