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 3840 e0baea4d485a
parent 2539 ddd22ceee8cc
child 6053 8a1059aa01f0 
--- a/src/ZF/List.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/List.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -31,16 +31,16 @@
 
 constdefs
   hd      :: i=>i
-  "hd(l)       == list_case(0, %x xs.x, l)"
+  "hd(l)       == list_case(0, %x xs. x, l)"
   
   tl      :: i=>i
-  "tl(l)       == list_case(Nil, %x xs.xs, l)"
+  "tl(l)       == list_case(Nil, %x xs. xs, l)"
   
   drop       :: [i,i]=>i
   "drop(i,l)   == rec(i, l, %j r. tl(r))"
 
   list_rec   :: [i, i, [i,i,i]=>i] => i
-  "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
+  "list_rec(l,c,h) == Vrec(l, %l g. list_case(c, %x xs. h(x, xs, g`xs), l))"
 
   map        :: [i=>i, i] => i
   "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
isabelle