src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
changeset 52666 391913d17d15
parent 46905 6b1c0a80a57a
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Mon Jul 15 20:13:30 2013 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Mon Jul 15 20:36:27 2013 +0200
     1.3 @@ -31,7 +31,9 @@
     1.4  
     1.5  lemma [code_pred_def]:
     1.6    "cardsp [] g k = False"
     1.7 -  "cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
     1.8 +  "cardsp (e # s) g k =
     1.9 +    (let C = cardsp s g
    1.10 +     in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
    1.11  unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)
    1.12  
    1.13  definition
    1.14 @@ -79,7 +81,10 @@
    1.15  
    1.16  values 40 "{s. hotel s}"
    1.17  
    1.18 -setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
    1.19 +setup {*
    1.20 +  Context.theory_map
    1.21 +    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    1.22 +*}
    1.23  
    1.24  lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
    1.25  quickcheck[tester = prolog, iterations = 1, expect = counterexample]