src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 39463 7ce0ed8dc4d6
parent 39302 d7728f65b353
child 39799 fdbea66eae4b
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 16 13:49:06 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 16 13:49:08 2010 +0200
     1.3 @@ -89,14 +89,12 @@
     1.4    limited_types = [],
     1.5    limited_predicates = [],
     1.6    replacing = [],
     1.7 -  manual_reorder = [],
     1.8 -  timeout = Time.fromSeconds 10,
     1.9 -  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.10 +  manual_reorder = []}) *}
    1.11  
    1.12  values 40 "{s. hotel s}"
    1.13  
    1.14  
    1.15 -setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
    1.16 +setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    1.17  
    1.18  lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    1.19  quickcheck[generator = code, iterations = 100000, report]
    1.20 @@ -119,9 +117,7 @@
    1.21     limited_types = [],
    1.22     limited_predicates = [(["hotel"], 5)],
    1.23     replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    1.24 -   manual_reorder = [],
    1.25 -   timeout = Time.fromSeconds 10,
    1.26 -   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.27 +   manual_reorder = []}) *}
    1.28  
    1.29  lemma
    1.30    "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"