isabelle: src/Doc/Tutorial/Misc/fakenat.thy@351810c45a48 (annotated)

8745 13b32661dde4 I wonder which files i forgot. nipkow parents: diff changeset	1	(<)
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 11418 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	haftmann
	Thu, 11 Sep 2014 23:12:32 +0200
changeset 58320	351810c45a48
parent 56260	3d79c132e657
child 58860	fee7cfa69c50
permissions	-rw-r--r--