src/HOL/ex/Primrec.thy
changeset 11464 ddea204de5bc
parent 11024 23bf8d787b04
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/ex/Primrec.thy	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/ex/Primrec.thy	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -159,7 +159,7 @@
     1.4  
     1.5  text {* PROPERTY A 8 *}
     1.6  
     1.7 -lemma ack_1 [simp]: "ack (1, j) = j + #2"
     1.8 +lemma ack_1 [simp]: "ack (1', j) = j + #2"
     1.9    apply (induct j)
    1.10     apply simp_all
    1.11    done