src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 38733 4b8fd91ea59a
parent 38731 2c8a595af43e
child 38734 e5508a74b11f
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:51 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:51 2010 +0200
     1.3 @@ -89,5 +89,13 @@
     1.4  values 10 "{s. hotel s}"
     1.5  
     1.6  
     1.7 +setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
     1.8 +ML {* set Code_Prolog.trace *}
     1.9 +
    1.10 +lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    1.11 +quickcheck[generator = code, iterations = 100000, report]
    1.12 +quickcheck[generator = prolog, iterations = 1]
    1.13 +oops
    1.14 +
    1.15  
    1.16  end
    1.17 \ No newline at end of file