# HG changeset patch
# User berghofe
# Date 958404619 -7200
# Node ID ab920d8112b4713905a0e529dae592985a8a42b9
# Parent  0ff5d55205a4b64084af523728540d30242a58d9
Removed unnecessary primrec equations of hd and last involving arbitrary.

diff -r 0ff5d55205a4 -r ab920d8112b4 src/HOL/List.thy
--- 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 [] = []"