isabelle: src/ZF/AC/Transrec2.thy@2b8c2a7547ab (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/AC/Transrec2.thy
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Krzysztof Grabczewski
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	4
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	5	Transfinite recursion introduced to handle definitions based on the three
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	6	cases of ordinals.
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	7	*)
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	8
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	9	Transrec2 = OrdQuant + Epsilon +
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	10
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	11	consts
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	12
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 1203 diff changeset	13	transrec2 :: [i, i, [i,i]=>i] =>i
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	14
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	15	defs
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	16
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	17	transrec2_def "transrec2(alpha, a, b) ==
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	18	transrec(alpha, %i r. if(i=0,
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	19	a, if(EX j. i=succ(j),
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	20	b(THE j. i=succ(j), r`(THE j. i=succ(j))),
2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	21	UN j<i. r`j)))"
992 4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	22
4ef4f7ff2aeb New example of AC Equivalences by Krzysztof Grabczewski lcp parents: diff changeset	23	end

author	clasohm
	Tue, 06 Feb 1996 12:27:17 +0100
changeset 1478	2b8c2a7547ab
parent 1401	0c439768f45c
permissions	-rw-r--r--