src/ZF/Coind/Types.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
     1.1 --- a/src/ZF/Coind/Types.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/Coind/Types.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,14 +1,14 @@
     1.4 -(*  Title: 	ZF/Coind/Types.thy
     1.5 +(*  Title:      ZF/Coind/Types.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
     1.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
     1.9      Copyright   1995  University of Cambridge
    1.10  *)
    1.11  
    1.12  Types = Language +
    1.13  
    1.14  consts
    1.15 -  Ty :: i			(* Datatype of types *)
    1.16 -  TyConst :: i		(* Abstract type of type constants *)
    1.17 +  Ty :: i                       (* Datatype of types *)
    1.18 +  TyConst :: i          (* Abstract type of type constants *)
    1.19  datatype <= "univ(TyConst)"
    1.20    "Ty" = t_const("tc:TyConst")
    1.21         | t_fun("t1:Ty","t2:Ty")