isabelle: src/HOL/Nat.thy@f72e58a5a75f (annotated)

923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	1	(* Title: HOL/Nat.thy
21243 afffe1f72143 removed theory NatArith (now part of Nat); wenzelm parents: 21191 diff changeset	2	Author: Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	3
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	4	Type "nat" is a linear order, and a datatype; arithmetic operators + -
30496 7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement haftmann parents: 30242 diff changeset	5	and * (for div and mod, see theory Divides).
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	6	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7
13449 43c9ec498291 - Converted to new theory format berghofe parents: 12338 diff changeset	8	header {* Natural numbers *}
43c9ec498291 - Converted to new theory format berghofe parents: 12338 diff changeset	9
15131 c69542757a4d New theory header syntax. nipkow parents: 14740 diff changeset	10	theory Nat
35121 36c0a6dd8c6f tuned import order haftmann parents: 35064 diff changeset	11	imports Inductive Typedef Fun Fields
15131 c69542757a4d New theory header syntax. nipkow parents: 14740 diff changeset	12	begin
13449 43c9ec498291 - Converted to new theory format berghofe parents: 12338 diff changeset	13
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48560 diff changeset	14	ML_file "~~/src/Tools/rat.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48560

author	hoelzl
	Tue, 12 Nov 2013 19:28:52 +0100
changeset 54411	f72e58a5a75f
parent 54223	85705ba18add
child 54496	178922b63b58
permissions	-rw-r--r--