# HG changeset patch
# User haftmann
# Date 1241706154 -7200
# Node ID 878e00798148f5ee6fe61e4106d25f5637d07f75
# Parent  1d117af9f9f36237d72a93be3eeb1499c416ff92
no need for explicit delete declaration

diff -r 1d117af9f9f3 -r 878e00798148 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Thu May 07 16:22:34 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy	Thu May 07 16:22:34 2009 +0200
@@ -10,7 +10,6 @@
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code nbe]
 lemma "((P | Q) | R) = (P | (Q | R))" by normalization
-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