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.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.13  definition
1.14 @@ -79,7 +81,10 @@
1.16  values 40 "{s. hotel s}"
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.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]