--- a/src/Doc/Tutorial/Misc/fakenat.thy Sun Mar 23 15:46:21 2014 +0100
+++ b/src/Doc/Tutorial/Misc/fakenat.thy Sun Mar 23 16:40:35 2014 +0100
@@ -4,10 +4,11 @@
text{*\noindent
The type \tydx{nat} of natural
-numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this:
+numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}.
+It behaves approximately as if it were declared like this:
*}
-datatype nat = 0 | Suc nat
+datatype nat = zero ("0") | Suc nat
(*<*)
end
(*>*)