isabelle: src/ZF/Ordinal.thy@073116d65bb9 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/Ordinal.thy
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	4	Copyright 1994 University of Cambridge
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	5
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	6	Ordinals in Zermelo-Fraenkel Set Theory
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	7	*)
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	8
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1478 diff changeset	9	Ordinal = WF + Bool + equalities +
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	10	consts
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	11	Memrel :: i=>i
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 852 diff changeset	12	Transset,Ord :: i=>o
0c439768f45c removed quotes from consts and syntax sections clasohm parents: 852 diff changeset	13	"<" :: [i,i] => o (infixl 50) (less than on ordinals)
2539 ddd22ceee8cc turned some consts into syntax; wenzelm parents: 2469 diff changeset	14	Limit :: i=>o
ddd22ceee8cc turned some consts into syntax; wenzelm parents: 2469 diff changeset	15
ddd22ceee8cc turned some consts into syntax; wenzelm parents: 2469 diff changeset	16	syntax
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 852 diff changeset	17	"le" :: [i,i] => o (infixl 50) (less than or equals)
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	18
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	19	translations
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	20	"x le y" == "x < succ(y)"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	21
12114 a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 2540 diff changeset	22	syntax (xsymbols)
2540 ba8311047f18 added symbols syntax; wenzelm parents: 2539 diff changeset	23	"op le" :: [i,i] => o (infixl "\\<le>" 50) (less than or equals)
ba8311047f18 added symbols syntax; wenzelm parents: 2539 diff changeset	24
753 ec86863e87c8 replaced "rules" by "defs" lcp parents: 435 diff changeset	25	defs
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	26	Memrel_def "Memrel(A) == {z: A*A . EX x y. z=<x,y> & x:y }"
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	27	Transset_def "Transset(i) == ALL x:i. x<=i"
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	28	Ord_def "Ord(i) == Transset(i) & (ALL x:i. Transset(x))"
435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	29	lt_def "i<j == i:j & Ord(j)"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	30	Limit_def "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	31
ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset	32	end

author	berghofe
	Mon, 21 Jan 2002 14:43:38 +0100
changeset 12822	073116d65bb9
parent 12114	a8e860c86252
child 13155	dcbf6cb95534
permissions	-rw-r--r--