isabelle: src/ZF/ord.thy@a5a9c433f639 (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: ZF/ordinal.thy
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Ordinals in Zermelo-Fraenkel Set Theory
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	Ord = WF +
a5a9c433f639 Initial revision clasohm parents: diff changeset	10	consts
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	Memrel :: "i=>i"
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	Transset,Ord :: "i=>o"
a5a9c433f639 Initial revision clasohm parents: diff changeset	13
a5a9c433f639 Initial revision clasohm parents: diff changeset	14	rules
a5a9c433f639 Initial revision clasohm parents: diff changeset	15	Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"
a5a9c433f639 Initial revision clasohm parents: diff changeset	16	Transset_def "Transset(i) == ALL x:i. x<=i"
a5a9c433f639 Initial revision clasohm parents: diff changeset	17	Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"
a5a9c433f639 Initial revision clasohm parents: diff changeset	18
a5a9c433f639 Initial revision clasohm parents: diff changeset	19	end

author	clasohm
	Thu, 16 Sep 1993 12:20:38 +0200
changeset 0	a5a9c433f639
child 30	d49df4181f0d
permissions	-rw-r--r--