Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/NormalForm.thy
changeset 28709 6a5d214aaa82
parent 28562 4e74209f113e
child 28952 15a4b2cf8c34 
--- a/src/HOL/ex/NormalForm.thy	Wed Oct 29 11:33:40 2008 +0100
+++ b/src/HOL/ex/NormalForm.thy	Wed Oct 29 15:32:58 2008 +0100
@@ -34,7 +34,7 @@
   "add2 (S m) n = S(add2 m n)"
 
 declare add2.simps [code]
-lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)"
+lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
   by (induct n) auto
 lemma [code]: "add2 n (S m) =  S (add2 n m)"
   by(induct n) auto
isabelle