src/HOL/Nitpick.thy
changeset 61799 4cf66f21b764
parent 61681 ca53150406c9
child 61944 5d06ecfdb472
     1.1 --- a/src/HOL/Nitpick.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -116,7 +116,7 @@
     1.4  
     1.5  text \<open>
     1.6  Auxiliary definitions used to provide an alternative representation for
     1.7 -@{text rat} and @{text real}.
     1.8 +\<open>rat\<close> and \<open>real\<close>.
     1.9  \<close>
    1.10  
    1.11  function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where