--- a/src/ZF/ex/Brouwer.thy Fri Nov 16 22:10:27 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: ZF/ex/Brouwer.thy
- ID: $ $
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Infinite branching datatype definitions
- (1) the Brouwer ordinals
- (2) the Martin-Löf wellordering type
-*)
-
-Brouwer = Main +
-
-consts
- brouwer :: i
- Well :: [i,i=>i]=>i
-
-datatype <= "Vfrom(0, csucc(nat))"
- "brouwer" = Zero | Suc ("b \\<in> brouwer") | Lim ("h \\<in> nat -> brouwer")
- monos Pi_mono
- type_intrs "inf_datatype_intrs"
-
-(*The union with nat ensures that the cardinal is infinite*)
-datatype <= "Vfrom(A Un (\\<Union>x \\<in> A. B(x)), csucc(nat Un |\\<Union>x \\<in> A. B(x)|))"
- "Well(A,B)" = Sup ("a \\<in> A", "f \\<in> B(a) -> Well(A,B)")
- monos Pi_mono
- type_intrs "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]
- @ inf_datatype_intrs"
-
-
-end