# HG changeset patch
# User wenzelm
# Date 1395589235 -3600
# Node ID 3d79c132e657ebbf44be57b73167b1b5c4091de3
# Parent  0d301d91444bc10fcff7285703093a93f6096d11
modernized approximation, avoiding bad name binding;

diff -r 0d301d91444b -r 3d79c132e657 src/Doc/Tutorial/Misc/fakenat.thy
--- 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
 (*>*)