src/Doc/Datatypes/Datatypes.thy

 *}
 
     datatype_new nat = Zero | Suc nat
 
 text {*
-Setup to be able to write @{term 0} instead of @{const Zero}:
+Setup to be able to write @{text 0} instead of @{const Zero}:
 *}
 
     instantiation nat :: zero
     begin
     definition "0 = Zero"