| changeset 28143 | e5c6c4aac52c |
| parent 26739 | 947b6013e863 |
| child 28337 | 93964076e7b8 |
--- a/src/HOL/ex/NormalForm.thy Fri Sep 05 06:50:20 2008 +0200 +++ b/src/HOL/ex/NormalForm.thy Fri Sep 05 06:50:22 2008 +0200 @@ -32,8 +32,9 @@ "add2 Z n = n" "add2 (S m) n = S(add2 m n)" +declare add2.simps [code] lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)" - by(induct n) auto + by (induct n) auto lemma [code]: "add2 n (S m) = S (add2 n m)" by(induct n) auto lemma [code]: "add2 n Z = n"