src/ZF/ex/Brouwer.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6117 f9aad8ccd590
     1.1 --- a/src/ZF/ex/Brouwer.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/ex/Brouwer.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/ex/Brouwer.thy
     1.5 +(*  Title:      ZF/ex/Brouwer.thy
     1.6      ID:         $ $
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1994  University of Cambridge
    1.10  
    1.11  Infinite branching datatype definitions
    1.12 @@ -15,15 +15,15 @@
    1.13   
    1.14  datatype <= "Vfrom(0, csucc(nat))"
    1.15    "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
    1.16 -  monos	      "[Pi_mono]"
    1.17 +  monos       "[Pi_mono]"
    1.18    type_intrs  "inf_datatype_intrs"
    1.19  
    1.20  (*The union with nat ensures that the cardinal is infinite*)
    1.21  datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
    1.22    "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
    1.23 -  monos	      "[Pi_mono]"
    1.24 +  monos       "[Pi_mono]"
    1.25    type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   
    1.26 -	       @ inf_datatype_intrs"
    1.27 +               @ inf_datatype_intrs"
    1.28  
    1.29  
    1.30  end