src/ZF/List.thy
changeset 1401 0c439768f45c
parent 810 91c68f74f458
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/List.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/List.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -13,20 +13,20 @@
     1.4  List = Datatype + 
     1.5  
     1.6  consts
     1.7 -  "@"	     :: "[i,i]=>i"      			(infixr 60)
     1.8 -  list_rec   :: "[i, i, [i,i,i]=>i] => i"
     1.9 -  map 	     :: "[i=>i, i] => i"
    1.10 -  length,rev :: "i=>i"
    1.11 -  flat       :: "i=>i"
    1.12 -  list_add   :: "i=>i"
    1.13 -  hd,tl      :: "i=>i"
    1.14 -  drop	     :: "[i,i]=>i"
    1.15 +  "@"	     :: [i,i]=>i      			(infixr 60)
    1.16 +  list_rec   :: [i, i, [i,i,i]=>i] => i
    1.17 +  map 	     :: [i=>i, i] => i
    1.18 +  length,rev :: i=>i
    1.19 +  flat       :: i=>i
    1.20 +  list_add   :: i=>i
    1.21 +  hd,tl      :: i=>i
    1.22 +  drop	     :: [i,i]=>i
    1.23  
    1.24   (* List Enumeration *)
    1.25 - "[]"        :: "i" 	                           	("[]")
    1.26 - "@List"     :: "is => i" 	                   	("[(_)]")
    1.27 + "[]"        :: i 	                           	("[]")
    1.28 + "@List"     :: is => i 	                   	("[(_)]")
    1.29  
    1.30 -  list	     :: "i=>i"
    1.31 +  list	     :: i=>i
    1.32  
    1.33    
    1.34  datatype