--- a/src/HOL/ex/NormalForm.thy Tue Aug 08 08:19:15 2006 +0200
+++ b/src/HOL/ex/NormalForm.thy Tue Aug 08 08:19:18 2006 +0200
@@ -9,16 +9,8 @@
begin
lemma "p \<longrightarrow> True" by normalization
-
-(* FIXME Eventually the code generator should be able to handle this
-by re-generating the existing code for "or":
-
-declare disj_assoc[code]
-
-normal_form "(P | Q) | R"
-
-*)
-
+declare disj_assoc [code fun]
+normal_form "(P | Q) | R"
lemma "0 + (n::nat) = n" by normalization
lemma "0 + Suc(n) = Suc n" by normalization
@@ -104,7 +96,8 @@
normal_form "last[a,b,c]"
normal_form "last([a,b,c]@xs)"
-normal_form "max 0 x"
+normal_form "min 0 x"
+normal_form "min 0 (x::nat)"
text {*
Numerals still take their time\<dots>