--- 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
@@ -188,13 +188,23 @@
(*values "{x. one_or_two x}"*)
values [random] "{x. one_or_two x}"
-definition one_or_two':
- "one_or_two' == {1, (2::nat)}"
+inductive one_or_two' :: "nat => bool"
+where
+ "one_or_two' 1"
+| "one_or_two' 2"
+
+code_pred one_or_two' .
+thm one_or_two'.equation
-code_pred [inductify] one_or_two' .
-thm one_or_two'.equation
-(* TODO: handling numerals *)
-(*values "{x. one_or_two' x}"*)
+values "{x. one_or_two' x}"
+
+definition one_or_two'':
+ "one_or_two'' == {1, (2::nat)}"
+
+code_pred [inductify] one_or_two'' .
+thm one_or_two''.equation
+
+values "{x. one_or_two'' x}"
subsection {* even predicate *}