Mercurial Mercurial > repos > isabelle / 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.
Removed unnecessary primrec equations of hd and last involving arbitrary.
authorberghofe
Mon, 15 May 2000 17:30:19 +0200
changeset 8873 ab920d8112b4
parent 8872 0ff5d55205a4
child 8874 3242637f668c
Removed unnecessary primrec equations of hd and last involving arbitrary.
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Mon May 15 10:34:51 2000 +0200
+++ b/src/HOL/List.thy	Mon May 15 17:30:19 2000 +0200
@@ -83,13 +83,11 @@
 translations  "length"  =>  "size:: _ list => nat"
 
 primrec
-  "hd([]) = arbitrary"
   "hd(x#xs) = x"
 primrec
   "tl([]) = []"
   "tl(x#xs) = xs"
 primrec
-  "last [] = arbitrary"
   "last(x#xs) = (if xs=[] then x else last xs)"
 primrec
   "butlast [] = []"
isabelle