isabelle: src/Doc/Tutorial/Misc/fakenat.thy@67792e4a5486 (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
13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	5	text{*\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:
8745 13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	9	*}
13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	10
56260 3d79c132e657 modernized approximation, avoiding bad name binding; wenzelm parents: 48985 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	Manuel Eberl <eberlm@in.tum.de>
	Tue, 19 Jan 2016 07:59:29 +0100
changeset 62200	67792e4a5486
parent 58860	fee7cfa69c50
child 67406	23307fd33906
permissions	-rw-r--r--