Mercurial Mercurial > repos > Old_HOL / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added translations for "case xs of"
authornipkow
Sat, 12 Feb 1994 14:46:21 +0100
changeset 42 87f6e8b93221
parent 41 054ce38225b9
child 43 424c7b1489df
added translations for "case xs of"
List.thy file | annotate | diff | comparison | revisions 
--- a/List.thy	Fri Feb 11 11:09:50 1994 +0100
+++ b/List.thy	Sat Feb 12 14:46:21 1994 +0100
@@ -58,6 +58,8 @@
   "[x]"         == "Cons(x, [])"
   "[]"          == "Nil"
 
+  "case xs of Nil => a | Cons(y,ys) => b" == "list_case(xs,a,%y ys.b)"
+
   "[x:xs . P]"	== "filter(%x.P,xs)"
   "Alls x:xs.P"	== "list_all(%x.P,xs)"
Old_HOL