isabelle: src/HOL/Nat.thy@998cb95fdd43 (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
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	13	end

author	paulson
	Fri, 11 Apr 1997 15:21:36 +0200
changeset 2935	998cb95fdd43
parent 2608	450c9b682a92
child 3370	5c5fdce3a4e4
permissions	-rw-r--r--