--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Mon Jul 15 20:13:30 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Mon Jul 15 20:36:27 2013 +0200
@@ -19,7 +19,10 @@
declare size_list_def[symmetric, code_pred_inline]
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+ Context.theory_map
+ (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
datatype alphabet = a | b
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy Mon Jul 15 20:13:30 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy Mon Jul 15 20:36:27 2013 +0200
@@ -29,7 +29,8 @@
(s1 @ rhs @ s2) = rsl \<and>
(rule lhs rhs) \<in> fst g }"
-definition derivesp :: "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
+definition derivesp ::
+ "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
where
"derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))"
@@ -252,7 +253,8 @@
where
irconst: "eval_var (IrConst i) conf (IntVal i)"
| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
-| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
+| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow>
+ eval_var (Add l r) conf (IntVal (vl+vr))"
code_pred eval_var .
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Mon Jul 15 20:13:30 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Mon Jul 15 20:36:27 2013 +0200
@@ -31,7 +31,9 @@
lemma [code_pred_def]:
"cardsp [] g k = False"
- "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)"
+ "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)"
unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)
definition
@@ -79,7 +81,10 @@
values 40 "{s. hotel s}"
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+ Context.theory_map
+ (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
quickcheck[tester = prolog, iterations = 1, expect = counterexample]
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Mon Jul 15 20:13:30 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Mon Jul 15 20:36:27 2013 +0200
@@ -79,7 +79,10 @@
section {* Manual setup to find counterexample *}
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+ Context.theory_map
+ (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
setup {* Code_Prolog.map_code_options (K
{ ensure_groundness = true,
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Mon Jul 15 20:13:30 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Mon Jul 15 20:36:27 2013 +0200
@@ -5,7 +5,10 @@
"~~/src/HOL/Library/Code_Prolog"
begin
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+ Context.theory_map
+ (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Jul 15 20:13:30 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Jul 15 20:36:27 2013 +0200
@@ -85,7 +85,8 @@
fun prop_regex :: "Nat * Nat * RE * RE * Sym list \<Rightarrow> bool"
where
- "prop_regex (n, (k, (p, (q, s)))) = ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
+ "prop_regex (n, (k, (p, (q, s)))) =
+ ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
@@ -97,7 +98,10 @@
oops
-setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
+setup {*
+ Context.theory_map
+ (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
+*}
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,