Removed unnecessary primrec equations of hd and last involving arbitrary.
authorberghofe
Mon May 15 17:30:19 2000 +0200 (2000-05-15)
changeset 8873ab920d8112b4
parent 8872 0ff5d55205a4
child 8874 3242637f668c
Removed unnecessary primrec equations of hd and last involving arbitrary.
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Mon May 15 10:34:51 2000 +0200
     1.2 +++ b/src/HOL/List.thy	Mon May 15 17:30:19 2000 +0200
     1.3 @@ -83,13 +83,11 @@
     1.4  translations  "length"  =>  "size:: _ list => nat"
     1.5  
     1.6  primrec
     1.7 -  "hd([]) = arbitrary"
     1.8    "hd(x#xs) = x"
     1.9  primrec
    1.10    "tl([]) = []"
    1.11    "tl(x#xs) = xs"
    1.12  primrec
    1.13 -  "last [] = arbitrary"
    1.14    "last(x#xs) = (if xs=[] then x else last xs)"
    1.15  primrec
    1.16    "butlast [] = []"