--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Wed Aug 25 16:59:51 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Wed Aug 25 16:59:51 2010 +0200
@@ -89,5 +89,13 @@
values 10 "{s. hotel s}"
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+ML {* set Code_Prolog.trace *}
+
+lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
+quickcheck[generator = code, iterations = 100000, report]
+quickcheck[generator = prolog, iterations = 1]
+oops
+
end
\ No newline at end of file