isabelle: src/HOL/Nat.thy@5b8c0c8f576e (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
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	6	Nat is a partial order
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
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	9	Nat = NatDef +
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	11	instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
1660 8cb42cd97579 * empty log message * oheimb parents: 1625 diff changeset	12
3370 5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	13	consts
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	14	"^" :: ['a::power,nat] => 'a (infixr 80)
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	15
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	16	end

author	paulson
	Fri, 19 Sep 1997 16:12:21 +0200
changeset 3685	5b8c0c8f576e
parent 3370	5c5fdce3a4e4
child 4104	84433b1ab826
permissions	-rw-r--r--