src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 38949 1afa9e89c885
parent 38734 e5508a74b11f
child 38950 62578950e748
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:51 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:52 2010 +0200
     1.3 @@ -84,17 +84,21 @@
     1.4  lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
     1.5  by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
     1.6  
     1.7 -ML {* Code_Prolog.options := {ensure_groundness = true} *}
     1.8 +ML {* Code_Prolog.options :=
     1.9 +  {ensure_groundness = true,
    1.10 +  limited_types = [],
    1.11 +  limited_predicates = [],
    1.12 +  replacing = [],
    1.13 +  prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.14  
    1.15  values 40 "{s. hotel s}"
    1.16  
    1.17  
    1.18  setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
    1.19 -ML {* set Code_Prolog.trace *}
    1.20  
    1.21  lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    1.22  quickcheck[generator = code, iterations = 100000, report]
    1.23 -quickcheck[generator = prolog, iterations = 1]
    1.24 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    1.25  oops
    1.26  
    1.27