| changeset 28562 | 4e74209f113e |
| parent 28422 | bfa368164502 |
| child 28709 | 6a5d214aaa82 |
--- a/src/HOL/ex/NormalForm.thy Fri Oct 10 06:45:50 2008 +0200 +++ b/src/HOL/ex/NormalForm.thy Fri Oct 10 06:45:53 2008 +0200 @@ -12,7 +12,7 @@ lemma "p \<longrightarrow> True" by normalization declare disj_assoc [code nbe] lemma "((P | Q) | R) = (P | (Q | R))" by normalization -declare disj_assoc [code func del] +declare disj_assoc [code 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