
diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -276,7 +276,7 @@
 by (descending) (auto intro: int_induct2)
   
 
-text \<open>Magnitide of an Integer, as a Natural Number: @{term nat}\<close>
+text \<open>Magnitide of an Integer, as a Natural Number: \<^term>\<open>nat\<close>\<close>
 
 definition
   "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"




