src/ZF/ex/Brouwer.thy
changeset 6117 f9aad8ccd590
parent 1478 2b8c2a7547ab
child 11316 b4e71bd751e4
     1.1 --- a/src/ZF/ex/Brouwer.thy	Wed Jan 13 12:44:33 1999 +0100
     1.2 +++ b/src/ZF/ex/Brouwer.thy	Wed Jan 13 15:14:47 1999 +0100
     1.3 @@ -15,13 +15,13 @@
     1.4   
     1.5  datatype <= "Vfrom(0, csucc(nat))"
     1.6    "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
     1.7 -  monos       "[Pi_mono]"
     1.8 +  monos        Pi_mono
     1.9    type_intrs  "inf_datatype_intrs"
    1.10  
    1.11  (*The union with nat ensures that the cardinal is infinite*)
    1.12  datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
    1.13    "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
    1.14 -  monos       "[Pi_mono]"
    1.15 +  monos        Pi_mono
    1.16    type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   
    1.17                 @ inf_datatype_intrs"
    1.18