diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Thu May 26 17:51:22 2016 +0200
@@ -3,7 +3,7 @@
     Copyright   2011 TU Muenchen
 *)
 
-section {* Examples for narrowing-based testing  *}
+section \<open>Examples for narrowing-based testing\<close>
 
 theory Quickcheck_Narrowing_Examples
 imports Main
@@ -11,7 +11,7 @@
 
 declare [[quickcheck_timeout = 3600]]
 
-subsection {* Minimalistic examples *}
+subsection \<open>Minimalistic examples\<close>
 
 lemma
   "x = y"
@@ -23,7 +23,7 @@
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
 oops
 
-subsection {* Simple examples with existentials *}
+subsection \<open>Simple examples with existentials\<close>
 
 lemma
   "\<exists> y :: nat. \<forall> x. x = y"
@@ -50,19 +50,19 @@
 quickcheck[tester = narrowing, finite_types = false, size = 7]
 oops
 
-text {* A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp} *}
+text \<open>A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp}\<close>
 lemma
   "~ distinct ws ==> EX xs ys zs y. ws = xs @ [y] @ ys @ [y]"
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
 oops
 
-text {* A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last} *}  
+text \<open>A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last}\<close>  
 lemma
   "x : set xs ==> EX ys zs. xs = ys @ x # zs & x ~: set zs & x ~: set ys"
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
 oops
 
-text {* A false conjecture derived from @{thm map_eq_Cons_conv} with a typo *}
+text \<open>A false conjecture derived from @{thm map_eq_Cons_conv} with a typo\<close>
 lemma
   "(map f xs = y # ys) = (EX z zs. xs = z' # zs & f z = y & map f zs = ys)"
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
@@ -73,7 +73,7 @@
 quickcheck[exhaustive, random, expect = no_counterexample]
 oops
 
-subsection {* Simple list examples *}
+subsection \<open>Simple list examples\<close>
 
 lemma "rev xs = xs"
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
@@ -87,7 +87,7 @@
   quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
 oops
 
-subsection {* Simple examples with functions *}
+subsection \<open>Simple examples with functions\<close>
 
 lemma "map f xs = map g xs"
   quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
@@ -117,7 +117,7 @@
 oops
 *)
 
-subsection {* Simple examples with inductive predicates *}
+subsection \<open>Simple examples with inductive predicates\<close>
 
 inductive even where
   "even 0" |
@@ -130,7 +130,7 @@
 oops
 
 
-subsection {* AVL Trees *}
+subsection \<open>AVL Trees\<close>
 
 datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
 
@@ -204,7 +204,7 @@
                  else MKT n l r' (1 + max hl hr'))"
 
 
-subsubsection {* Necessary setup for code generation *}
+subsubsection \<open>Necessary setup for code generation\<close>
 
 primrec set_of'
 where 
@@ -221,14 +221,14 @@
 
 declare is_ord.simps(1)[code] is_ord_mkt[code]
 
-subsubsection {* Invalid Lemma due to typo in @{const l_bal} *}
+subsubsection \<open>Invalid Lemma due to typo in @{const l_bal}\<close>
 
 lemma is_ord_l_bal:
  "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, expect = counterexample]
 oops
 
-subsection {* Examples with hd and last *}
+subsection \<open>Examples with hd and last\<close>
 
 lemma
   "hd (xs @ ys) = hd ys"
@@ -240,7 +240,7 @@
 quickcheck[narrowing, expect = counterexample]
 oops
 
-subsection {* Examples with underspecified/partial functions *}
+subsection \<open>Examples with underspecified/partial functions\<close>
 
 lemma
   "xs = [] ==> hd xs \<noteq> x"