--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu May 26 17:51:22 2016 +0200
@@ -4,10 +4,10 @@
"~~/src/HOL/Library/Code_Prolog"
begin
-text {* An example from the experiments from SmallCheck (@{url "http://www.cs.york.ac.uk/fp/smallcheck/"}) *}
-text {* The example (original in Haskell) was imported with Haskabelle and
+text \<open>An example from the experiments from SmallCheck (@{url "http://www.cs.york.ac.uk/fp/smallcheck/"})\<close>
+text \<open>The example (original in Haskell) was imported with Haskabelle and
manually slightly adapted.
-*}
+\<close>
datatype Nat = Zer
| Suc Nat
@@ -98,12 +98,12 @@
oops
-setup {*
+setup \<open>
Context.theory_map
(Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
-*}
+\<close>
-setup {* Code_Prolog.map_code_options (K
+setup \<open>Code_Prolog.map_code_options (K
{ensure_groundness = true,
limit_globally = NONE,
limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
@@ -114,10 +114,10 @@
(("subP", "limited_subP"), "repIntP"),
(("repIntPa", "limited_repIntPa"), "repIntP"),
(("accepts", "limited_accepts"), "quickcheck")],
- manual_reorder = []}) *}
+ manual_reorder = []})\<close>
-text {* Finding the counterexample still seems out of reach for the
- prolog-style generation. *}
+text \<open>Finding the counterexample still seems out of reach for the
+ prolog-style generation.\<close>
lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
quickcheck[exhaustive]
@@ -127,7 +127,7 @@
(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
oops
-section {* Given a partial solution *}
+section \<open>Given a partial solution\<close>
lemma
(* assumes "n = Zer"
@@ -140,7 +140,7 @@
quickcheck[tester = prolog, iterations = 1, size = 1]
oops
-section {* Checking the counterexample *}
+section \<open>Checking the counterexample\<close>
definition a_sol
where