Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/List.thy
changeset 1401 0c439768f45c
parent 810 91c68f74f458
child 1478 2b8c2a7547ab 
--- a/src/ZF/List.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/List.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -13,20 +13,20 @@
 List = Datatype + 
 
 consts
-  "@"	     :: "[i,i]=>i"      			(infixr 60)
-  list_rec   :: "[i, i, [i,i,i]=>i] => i"
-  map 	     :: "[i=>i, i] => i"
-  length,rev :: "i=>i"
-  flat       :: "i=>i"
-  list_add   :: "i=>i"
-  hd,tl      :: "i=>i"
-  drop	     :: "[i,i]=>i"
+  "@"	     :: [i,i]=>i      			(infixr 60)
+  list_rec   :: [i, i, [i,i,i]=>i] => i
+  map 	     :: [i=>i, i] => i
+  length,rev :: i=>i
+  flat       :: i=>i
+  list_add   :: i=>i
+  hd,tl      :: i=>i
+  drop	     :: [i,i]=>i
 
  (* List Enumeration *)
- "[]"        :: "i" 	                           	("[]")
- "@List"     :: "is => i" 	                   	("[(_)]")
+ "[]"        :: i 	                           	("[]")
+ "@List"     :: is => i 	                   	("[(_)]")
 
-  list	     :: "i=>i"
+  list	     :: i=>i
 
   
 datatype
isabelle