src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 38734 e5508a74b11f
parent 38733 4b8fd91ea59a
child 38949 1afa9e89c885
     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:53 2010 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  | "hotel (e # s) = (hotel s & (case e of
     1.5    Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
     1.6    Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
     1.7 -  Exit g r \<Rightarrow> False))"
     1.8 +  Exit g r \<Rightarrow> g : isin s r))"
     1.9  
    1.10  lemma issued_nil: "issued [] = {Key0}"
    1.11  by (auto simp add: initk_def)
    1.12 @@ -86,7 +86,7 @@
    1.13  
    1.14  ML {* Code_Prolog.options := {ensure_groundness = true} *}
    1.15  
    1.16 -values 10 "{s. hotel s}"
    1.17 +values 40 "{s. hotel s}"
    1.18  
    1.19  
    1.20  setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}