| changeset 22845 | 5f9138bcb3d7 |
| parent 22394 | 54ea68b5a92f |
| child 23396 | 6d72ababc58f |
--- a/src/HOL/ex/NormalForm.thy Sun May 06 21:49:44 2007 +0200 +++ b/src/HOL/ex/NormalForm.thy Sun May 06 21:50:17 2007 +0200 @@ -13,7 +13,7 @@ lemma "p \<longrightarrow> True" by normalization declare disj_assoc [code func] lemma "((P | Q) | R) = (P | (Q | R))" by normalization -declare disj_assoc [code nofunc] +declare disj_assoc [code func del] lemma "0 + (n::nat) = n" by normalization lemma "0 + Suc n = Suc n" by normalization lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization