src/ZF/ex/Brouwer.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/ex/Brouwer.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/ex/Brouwer.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4  
     1.5  Brouwer = InfDatatype +
     1.6  consts
     1.7 -  brouwer :: "i"
     1.8 -  Well    :: "[i,i=>i]=>i"
     1.9 +  brouwer :: i
    1.10 +  Well    :: [i,i=>i]=>i
    1.11   
    1.12  datatype <= "Vfrom(0, csucc(nat))"
    1.13    "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")