diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu May 26 17:51:22 2016 +0200
@@ -5,7 +5,7 @@
 Examples from the Nitpick manual.
 *)
 
-section {* Examples from the Nitpick Manual *}
+section \<open>Examples from the Nitpick Manual\<close>
 
 (* The "expect" arguments to Nitpick in this theory and the other example
    theories are there so that the example can also serve as a regression test
@@ -15,12 +15,12 @@
 imports Real "~~/src/HOL/Library/Quotient_Product"
 begin
 
-section {* 2. First Steps *}
+section \<open>2. First Steps\<close>
 
 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 
-subsection {* 2.1. Propositional Logic *}
+subsection \<open>2.1. Propositional Logic\<close>
 
 lemma "P \<longleftrightarrow> Q"
 nitpick [expect = genuine]
@@ -30,14 +30,14 @@
 oops
 
 
-subsection {* 2.2. Type Variables *}
+subsection \<open>2.2. Type Variables\<close>
 
 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [verbose, expect = genuine]
 oops
 
 
-subsection {* 2.3. Constants *}
+subsection \<open>2.3. Constants\<close>
 
 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [show_consts, expect = genuine]
@@ -51,7 +51,7 @@
 by (metis the_equality)
 
 
-subsection {* 2.4. Skolemization *}
+subsection \<open>2.4. Skolemization\<close>
 
 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
 nitpick [expect = genuine]
@@ -66,7 +66,7 @@
 oops
 
 
-subsection {* 2.5. Natural Numbers and Integers *}
+subsection \<open>2.5. Natural Numbers and Integers\<close>
 
 lemma "\<lbrakk>i \<le> j; n \<le> (m::int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
 nitpick [expect = genuine]
@@ -87,7 +87,7 @@
 oops
 
 
-subsection {* 2.6. Inductive Datatypes *}
+subsection \<open>2.6. Inductive Datatypes\<close>
 
 lemma "hd (xs @ [y, y]) = hd xs"
 nitpick [expect = genuine]
@@ -99,7 +99,7 @@
 oops
 
 
-subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
+subsection \<open>2.7. Typedefs, Records, Rationals, and Reals\<close>
 
 definition "three = {0::nat, 1, 2}"
 typedef three = three
@@ -129,16 +129,16 @@
 nitpick [show_types, expect = genuine]
 oops
 
-ML {*
+ML \<open>
 fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
     HOLogic.mk_number T (snd (HOLogic.dest_number t1)
                          - snd (HOLogic.dest_number t2))
   | my_int_postproc _ _ _ _ t = t
-*}
+\<close>
 
-declaration {*
+declaration \<open>
 Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
-*}
+\<close>
 
 lemma "add x y = add x x"
 nitpick [show_types]
@@ -157,7 +157,7 @@
 oops
 
 
-subsection {* 2.8. Inductive and Coinductive Predicates *}
+subsection \<open>2.8. Inductive and Coinductive Predicates\<close>
 
 inductive even where
 "even 0" |
@@ -200,7 +200,7 @@
 oops
 
 
-subsection {* 2.9. Coinductive Datatypes *}
+subsection \<open>2.9. Coinductive Datatypes\<close>
 
 codatatype 'a llist = LNil | LCons 'a "'a llist"
 
@@ -221,7 +221,7 @@
 sorry
 
 
-subsection {* 2.10. Boxing *}
+subsection \<open>2.10. Boxing\<close>
 
 datatype tm = Var nat | Lam tm | App tm tm
 
@@ -258,7 +258,7 @@
 sorry
 
 
-subsection {* 2.11. Scope Monotonicity *}
+subsection \<open>2.11. Scope Monotonicity\<close>
 
 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
 nitpick [verbose, expect = genuine]
@@ -270,7 +270,7 @@
 oops
 
 
-subsection {* 2.12. Inductive Properties *}
+subsection \<open>2.12. Inductive Properties\<close>
 
 inductive_set reach where
 "(4::nat) \<in> reach" |
@@ -299,12 +299,12 @@
 by (induct set: reach) arith+
 
 
-section {* 3. Case Studies *}
+section \<open>3. Case Studies\<close>
 
 nitpick_params [max_potential = 0]
 
 
-subsection {* 3.1. A Context-Free Grammar *}
+subsection \<open>3.1. A Context-Free Grammar\<close>
 
 datatype alphabet = a | b
 
@@ -379,7 +379,7 @@
 sorry
 
 
-subsection {* 3.2. AA Trees *}
+subsection \<open>3.2. AA Trees\<close>
 
 datatype 'a aa_tree = \<Lambda> | N "'a::linorder" nat "'a aa_tree" "'a aa_tree"