# HG changeset patch
# User haftmann
# Date 1155017958 -7200
# Node ID bb56a6cbacacbce0c23430e6e6841e687d88aae9
# Parent  c7658e811ffba6ea2815717feb4eefe15dbad5a1
adding code lemma now works as expected

diff -r c7658e811ffb -r bb56a6cbacac src/HOL/ex/NormalForm.thy
--- 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>