# HG changeset patch
# User wenzelm
# Date 1373913387 -7200
# Node ID 391913d17d1580f284faa661b3784edee9c635ae
# Parent  5f817bad850a6ab6174b61977490283a59c98e88
tuned line length;

diff -r 5f817bad850a -r 391913d17d15 src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
--- 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
 
diff -r 5f817bad850a -r 391913d17d15 src/HOL/Predicate_Compile_Examples/Examples.thy
--- 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 .
diff -r 5f817bad850a -r 391913d17d15 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- 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]
diff -r 5f817bad850a -r 391913d17d15 src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
--- 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,
diff -r 5f817bad850a -r 391913d17d15 src/HOL/Predicate_Compile_Examples/List_Examples.thy
--- 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,
diff -r 5f817bad850a -r 391913d17d15 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- 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,