src/HOL/ex/Primrec.thy
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))"