src/Doc/Tutorial/Misc/fakenat.thy
author wenzelm
Mon, 20 May 2024 15:43:51 +0200
changeset 80182 29f2b8ff84f3
parent 67406 23307fd33906
child 80914 d97fdabd9e2b
permissions -rw-r--r--
proper support for "isabelle update -D DIR": avoid accidental exclusion of select_dirs (amending e5dafe9e120f);

(*<*)
theory fakenat imports Main begin
(*>*)

text\<open>\noindent
The type \tydx{nat} of natural
numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}.
It behaves approximately as if it were declared like this:
\<close>

datatype nat = zero ("0") | Suc nat
(*<*)
end
(*>*)