--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Wed Apr 21 12:10:52 2010 +0200
@@ -1392,6 +1392,20 @@
values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"
+subsection {* minus on bool *}
+
+inductive All :: "nat => bool"
+where
+ "All x"
+
+inductive None :: "nat => bool"
+
+definition "test_minus_bool x = (None x - All x)"
+
+code_pred [inductify] test_minus_bool .
+thm test_minus_bool.equation
+
+values "{x. test_minus_bool x}"