src/HOL/Real.thy
changeset 67226 ec32cdaab97b
parent 67051 e7e54a0b9197
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Real.thy	Tue Dec 19 14:51:27 2017 +0100
     1.2 +++ b/src/HOL/Real.thy	Tue Dec 19 13:58:12 2017 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  subsection \<open>Preliminary lemmas\<close>
     1.6  
     1.7 -text{*Useful in convergence arguments*}
     1.8 +text\<open>Useful in convergence arguments\<close>
     1.9  lemma inverse_of_nat_le:
    1.10    fixes n::nat shows "\<lbrakk>n \<le> m; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 / of_nat m \<le> (1::'a::linordered_field) / of_nat n"
    1.11    by (simp add: frac_le)