Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no need for explicit delete declaration
authorhaftmann
Thu, 07 May 2009 16:22:34 +0200
changeset 31062 878e00798148
parent 31061 1d117af9f9f3
child 31063 88aaab83b6fc
no need for explicit delete declaration
src/HOL/ex/NormalForm.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle