# HG changeset patch # User paulson # Date 865585193 -7200 # Node ID 9092b79d86d50f4b4d408d00071772997f408df6 # Parent f060dc3f15a81c9817e7a6c2583eb32515dd3966 Mended the definition of ack(0,n) diff -r f060dc3f15a8 -r 9092b79d86d5 src/HOL/ex/Primrec.thy --- a/src/HOL/ex/Primrec.thy Fri Jun 06 10:19:20 1997 +0200 +++ b/src/HOL/ex/Primrec.thy Fri Jun 06 10:19:53 1997 +0200 @@ -20,7 +20,7 @@ consts ack :: "nat * nat => nat" recdef ack "less_than ** less_than" - "ack (0,n) = (n + 1)" + "ack (0,n) = Suc n" "ack (Suc m,0) = (ack (m, 1))" "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"