disabled upt example because of a problem due to overloaded constants with the predicate compiler
authorbulwahn
Fri, 06 Nov 2009 08:11:58 +0100
changeset 33480 dcfe9100e0a6
parent 33479 428ddcc16e7b
child 33481 030db03cb426
disabled upt example because of a problem due to overloaded constants with the predicate compiler
src/HOL/ex/Predicate_Compile_ex.thy
--- 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 .