src/HOL/ex/NormalForm.thy
changeset 28709 6a5d214aaa82
parent 28562 4e74209f113e
child 28952 15a4b2cf8c34
     1.1 --- a/src/HOL/ex/NormalForm.thy	Wed Oct 29 11:33:40 2008 +0100
     1.2 +++ b/src/HOL/ex/NormalForm.thy	Wed Oct 29 15:32:58 2008 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4    "add2 (S m) n = S(add2 m n)"
     1.5  
     1.6  declare add2.simps [code]
     1.7 -lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)"
     1.8 +lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
     1.9    by (induct n) auto
    1.10  lemma [code]: "add2 n (S m) =  S (add2 n m)"
    1.11    by(induct n) auto