# HG changeset patch
# User bulwahn
# Date 1256630636 -3600
# Node ID d9ca0c3bf680e914c826ef4c2f10dcd70860fffb
# Parent  8bd2eb003b8f87cd61b7bdf32c47439574add628
changes to example file

diff -r 8bd2eb003b8f -r d9ca0c3bf680 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Oct 27 09:03:56 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Oct 27 09:03:56 2009 +0100
@@ -14,6 +14,11 @@
 
 code_pred (mode: [], [1]) EmptySet .
 
+definition EmptySet' :: "'a \<Rightarrow> bool"
+where "EmptySet' = {}"
+
+code_pred (mode: [], [1]) [inductify, show_intermediate_results] EmptySet' .
+
 inductive EmptyRel :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
 
 code_pred (mode: [], [1], [2], [1, 2]) EmptyRel .
@@ -447,13 +452,6 @@
 values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
 values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
 
-(*values [random] "{xys. test_lexord xys}"*)
-(*values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}"*)
-(*
-lemma "(u, v) : lexord less_than_nat ==> (x @ u, y @ v) : lexord less_than_nat"
-quickcheck[generator=pred_compile]
-oops
-*)
 lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
 
 code_pred [inductify] lexn .
@@ -469,9 +467,7 @@
 code_pred [inductify, rpred] lenlex .
 thm lenlex.rpred_equation
 
-thm lists.intros
 code_pred [inductify] lists .
-
 thm lists.equation
 
 subsection {* AVL Tree *}
@@ -510,8 +506,6 @@
 code_pred [inductify] is_ord .
 thm is_ord.equation
 
-code_pred [rpred] is_ord .
-thm is_ord.rpred_equation
 
 subsection {* Definitions about Relations *}
 
@@ -524,17 +518,17 @@
 (*TODO: *)
 declare Id_on_def[unfolded UNION_def, code_pred_def]
 
-code_pred [inductify] Id_on .
-thm Id_on.equation
+(*code_pred [inductify] Id_on .
+thm Id_on.equation*)
 code_pred [inductify] Domain .
 thm Domain.equation
 code_pred [inductify] Range .
-thm sym_def
+thm Range.equation
 code_pred [inductify] Field .
 declare Sigma_def[unfolded UNION_def, code_pred_def]
 declare refl_on_def[unfolded UNION_def, code_pred_def]
-code_pred [inductify] refl_on .
-thm refl_on.equation
+(*code_pred [inductify] refl_on .
+thm refl_on.equation*)
 code_pred [inductify] total_on .
 thm total_on.equation
 code_pred [inductify] antisym .