diff -r 25bd4745ee38 -r cac1add157e8 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 16:44:46 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 03 22:33:22 2014 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2009-2013
+    Copyright   2009-2014
 
 Examples from the Nitpick manual.
 *)
@@ -15,10 +15,12 @@
 imports Main Real "~~/src/HOL/Library/Quotient_Product"
 begin
 
-chapter {* 2. First Steps *}
+
+section {* 2. First Steps *}
 
 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
+
 subsection {* 2.1. Propositional Logic *}
 
 lemma "P \<longleftrightarrow> Q"
@@ -28,12 +30,14 @@
 nitpick [expect = genuine] 2
 oops
 
+
 subsection {* 2.2. Type Variables *}
 
 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [verbose, expect = genuine]
 oops
 
+
 subsection {* 2.3. Constants *}
 
 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
@@ -47,6 +51,7 @@
 (* sledgehammer *)
 by (metis the_equality)
 
+
 subsection {* 2.4. Skolemization *}
 
 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
@@ -61,6 +66,7 @@
 nitpick [expect = genuine]
 oops
 
+
 subsection {* 2.5. Natural Numbers and Integers *}
 
 lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
@@ -81,6 +87,7 @@
 nitpick [card nat = 2, expect = none]
 oops
 
+
 subsection {* 2.6. Inductive Datatypes *}
 
 lemma "hd (xs @ [y, y]) = hd xs"
@@ -92,6 +99,7 @@
 nitpick [show_datatypes, expect = genuine]
 oops
 
+
 subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
 
 definition "three = {0\<Colon>nat, 1, 2}"
@@ -149,6 +157,7 @@
 nitpick [show_datatypes, expect = genuine]
 oops
 
+
 subsection {* 2.8. Inductive and Coinductive Predicates *}
 
 inductive even where
@@ -191,6 +200,7 @@
 nitpick [card nat = 4, show_consts, expect = genuine]
 oops
 
+
 subsection {* 2.9. Coinductive Datatypes *}
 
 codatatype 'a llist = LNil | LCons 'a "'a llist"
@@ -211,6 +221,7 @@
 nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
+
 subsection {* 2.10. Boxing *}
 
 datatype tm = Var nat | Lam tm | App tm tm
@@ -247,6 +258,7 @@
 nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
+
 subsection {* 2.11. Scope Monotonicity *}
 
 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
@@ -258,6 +270,7 @@
 nitpick [expect = genuine]
 oops
 
+
 subsection {* 2.12. Inductive Properties *}
 
 inductive_set reach where
@@ -286,45 +299,12 @@
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
 by (induct set: reach) arith+
 
-datatype 'a bin_tree = Leaf 'a | Branch "'a bin_tree" "'a bin_tree"
-
-primrec labels where
-"labels (Leaf a) = {a}" |
-"labels (Branch t u) = labels t \<union> labels u"
-
-primrec swap where
-"swap (Leaf c) a b =
- (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
-"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
-
-lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
-(* nitpick *)
-proof (induct t)
-  case Leaf thus ?case by simp
-next
-  case (Branch t u) thus ?case
-  (* nitpick *)
-  nitpick [non_std, show_all, expect = genuine]
-oops
-
-lemma "labels (swap t a b) =
-       (if a \<in> labels t then
-          if b \<in> labels t then labels t else (labels t - {a}) \<union> {b}
-        else
-          if b \<in> labels t then (labels t - {b}) \<union> {a} else labels t)"
-(* nitpick *)
-proof (induct t)
-  case Leaf thus ?case by simp
-next
-  case (Branch t u) thus ?case
-  nitpick [non_std, card = 1\<emdash>4, expect = none]
-  by auto
-qed
 
 section {* 3. Case Studies *}
 
 nitpick_params [max_potential = 0]
 
+
 subsection {* 3.1. A Context-Free Grammar *}
 
 datatype alphabet = a | b
@@ -399,6 +379,7 @@
 nitpick [card = 1\<emdash>5, expect = none]
 sorry
 
+
 subsection {* 3.2. AA Trees *}
 
 datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"