isabelle: src/Doc/Tutorial/Misc/fakenat.thy@664c1a6cc8c1 (annotated)

8745 13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	1	(<)
58860 fee7cfa69c50 eliminated spurious semicolons; wenzelm parents: 56260 diff changeset	2	theory fakenat imports Main begin
8745 13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	3	(>)
13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	4
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58860 diff changeset	5	text\<open>\noindent
11418 53a402c10ba9 indexing tweaks paulson parents: 9541 diff changeset	6	The type \tydx{nat} of natural
56260 3d79c132e657 modernized approximation, avoiding bad name binding; wenzelm parents: 48985 diff changeset	7	numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}.
3d79c132e657 modernized approximation, avoiding bad name binding; wenzelm parents: 48985 diff changeset	8	It behaves approximately as if it were declared like this:
67406 23307fd33906 isabelle update_cartouches -c; wenzelm parents: 58860 diff changeset	9	\<close>
8745 13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	10
80983 2cc651d3ce8e partial revert of d97fdabd9e2b, to build old documentation more reliably; wenzelm parents: 80914 diff changeset	11	datatype nat = zero ("0") \| Suc nat
8745 13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	12	(<)
13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	13	end
13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	14	(>)

author	Thomas Lindae <thomas.lindae@in.tum.de>
	Wed, 17 Jul 2024 21:02:30 +0200
changeset 81077	664c1a6cc8c1
parent 80983	2cc651d3ce8e
permissions	-rw-r--r--