isabelle: src/HOL/Nat.thy@6e0f23304061 (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	rep_datatype nat
5714 b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5499 diff changeset	12	distinct Suc_not_Zero, Zero_not_Suc
b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5499 diff changeset	13	inject Suc_Suc_eq
5188 633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	14	induct nat_induct
4104 84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	15
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	16	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	17	instance nat :: linorder (nat_le_linear)
1660 8cb42cd97579 * empty log message * oheimb parents: 1625 diff changeset	18
3370 5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	19	consts
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	20	"^" :: ['a::power,nat] => 'a (infixr 80)
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	21
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	22	end

author	wenzelm
	Thu, 16 Mar 2000 00:35:27 +0100
changeset 8490	6e0f23304061
parent 7702	35c7e0df749f
child 9436	62bb04ab4b01
permissions	-rw-r--r--