disabled upt example because of a problem due to overloaded constants with the predicate compiler
--- a/src/HOL/ex/Predicate_Compile_ex.thy Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Fri Nov 06 08:11:58 2009 +0100
@@ -276,6 +276,7 @@
value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])"
value [code] "Predicate.the (append_3 ([]::int list))"
+
text {* tricky case with alternative rules *}
inductive append2
@@ -660,6 +661,7 @@
thm set_of.equation
code_pred [inductify] is_ord .
+thm is_ord_aux.equation
thm is_ord.equation
@@ -714,7 +716,7 @@
code_pred [inductify] take .
code_pred [inductify] drop .
code_pred [inductify] zip .
-code_pred [inductify] upt .
+(*code_pred [inductify] upt .*)
code_pred [inductify] remdups .
code_pred [inductify] remove1 .
code_pred [inductify] removeAll .