src/HOL/ex/Primrec.thy
changeset 5184 9b8547a9496a
parent 3419 9092b79d86d5
child 5717 0d28dbe484b6
     1.1 --- a/src/HOL/ex/Primrec.thy	Fri Jul 24 13:03:20 1998 +0200
     1.2 +++ b/src/HOL/ex/Primrec.thy	Fri Jul 24 13:19:38 1998 +0200
     1.3 @@ -25,12 +25,12 @@
     1.4      "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
     1.5  
     1.6  consts  list_add :: nat list => nat
     1.7 -primrec list_add list
     1.8 +primrec
     1.9    "list_add []     = 0"
    1.10    "list_add (m#ms) = m + list_add ms"
    1.11  
    1.12  consts  zeroHd  :: nat list => nat
    1.13 -primrec zeroHd list
    1.14 +primrec
    1.15    "zeroHd []     = 0"
    1.16    "zeroHd (m#ms) = m"
    1.17