changeset 8703 | 816d8f6513be |
parent 6481 | dbf2d9b3d6c8 |
child 11024 | 23bf8d787b04 |
--- a/src/HOL/ex/Primrec.thy Thu Apr 13 15:01:45 2000 +0200 +++ b/src/HOL/ex/Primrec.thy Thu Apr 13 15:01:50 2000 +0200 @@ -19,7 +19,7 @@ Primrec = Main + consts ack :: "nat * nat => nat" -recdef ack "less_than ** less_than" +recdef ack "less_than <*lex*> less_than" "ack (0,n) = Suc n" "ack (Suc m,0) = (ack (m, 1))" "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"