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