| changeset 6481 | dbf2d9b3d6c8 |
| parent 5717 | 0d28dbe484b6 |
| child 8703 | 816d8f6513be |
--- a/src/HOL/ex/Primrec.thy Thu Apr 22 13:03:46 1999 +0200 +++ b/src/HOL/ex/Primrec.thy Thu Apr 22 13:04:23 1999 +0200 @@ -16,7 +16,7 @@ Demonstrates recursive definitions, the TFL package *) -Primrec = WF_Rel + List + +Primrec = Main + consts ack :: "nat * nat => nat" recdef ack "less_than ** less_than"