src/Doc/Tutorial/Misc/fakenat.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/Misc/fakenat.thy	Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,13 @@
+(*<*)
+theory fakenat imports Main begin;
+(*>*)
+
+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:
+*}
+
+datatype nat = 0 | Suc nat
+(*<*)
+end
+(*>*)