| changeset 20523 | 36a59e5d0039 |
| parent 20352 | bb56a6cbacac |
| child 20595 | db6bedfba498 |
--- a/src/HOL/ex/NormalForm.thy Wed Sep 13 00:38:38 2006 +0200 +++ b/src/HOL/ex/NormalForm.thy Wed Sep 13 12:05:50 2006 +0200 @@ -9,7 +9,7 @@ begin lemma "p \<longrightarrow> True" by normalization -declare disj_assoc [code fun] +declare disj_assoc [code func] normal_form "(P | Q) | R" lemma "0 + (n::nat) = n" by normalization