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

923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	1	(* Title: HOL/Nat.thy
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	3	Author: Tobias Nipkow
450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	4	Copyright 1997 TU Muenchen
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
5499 1787c44ae4ed updated comments paulson parents: 5188 diff changeset	6	Type "nat" is a linear order, and a datatype
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
5188 633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	9	Nat = NatDef + Inductive +
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10
5188 633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	11	setup
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	12	DatatypePackage.setup
4104 84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	13
5188 633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	14	rep_datatype nat
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	15	distinct "[[Suc_not_Zero, Zero_not_Suc]]"
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	16	inject "[[Suc_Suc_eq]]"
633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	17	induct nat_induct
4104 84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	18
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	19	instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4613 diff changeset	20	instance nat :: linorder (nat_le_linear)
1660 8cb42cd97579 * empty log message * oheimb parents: 1625 diff changeset	21
3370 5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	22	consts
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	23	"^" :: ['a::power,nat] => 'a (infixr 80)
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	24
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	25	end

author	paulson
	Thu, 01 Oct 1998 18:30:05 +0200
changeset 5601	b6456ccd9e3e
parent 5499	1787c44ae4ed
child 5714	b4f2e281a907
permissions	-rw-r--r--