1.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Sep 23 00:11:29 2011 +0200
     1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Sep 23 10:31:12 2011 +0200
     1.3 @@ -15,12 +15,12 @@
     1.4  imports Main "~~/src/HOL/Library/Quotient_Product" RealDef
     1.5  begin
     1.6  
     1.7 -chapter {* 3. First Steps *}
     1.8 +chapter {* 2. First Steps *}
     1.9  
    1.10  nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
    1.11                  timeout = 240]
    1.12  
    1.13 -subsection {* 3.1. Propositional Logic *}
    1.14 +subsection {* 2.1. Propositional Logic *}
    1.15  
    1.16  lemma "P \<longleftrightarrow> Q"
    1.17  nitpick [expect = genuine]
    1.18 @@ -29,13 +29,13 @@
    1.19  nitpick [expect = genuine] 2
    1.20  oops
    1.21  
    1.22 -subsection {* 3.2. Type Variables *}
    1.23 +subsection {* 2.2. Type Variables *}
    1.24  
    1.25  lemma "P x \<Longrightarrow> P (THE y. P y)"
    1.26  nitpick [verbose, expect = genuine]
    1.27  oops
    1.28  
    1.29 -subsection {* 3.3. Constants *}
    1.30 +subsection {* 2.3. Constants *}
    1.31  
    1.32  lemma "P x \<Longrightarrow> P (THE y. P y)"
    1.33  nitpick [show_consts, expect = genuine]
    1.34 @@ -49,7 +49,7 @@
    1.35  apply (metis the_equality)
    1.36  done
    1.37  
    1.38 -subsection {* 3.4. Skolemization *}
    1.39 +subsection {* 2.4. Skolemization *}
    1.40  
    1.41  lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
    1.42  nitpick [expect = genuine]
    1.43 @@ -63,7 +63,7 @@
    1.44  nitpick [expect = genuine]
    1.45  oops
    1.46  
    1.47 -subsection {* 3.5. Natural Numbers and Integers *}
    1.48 +subsection {* 2.5. Natural Numbers and Integers *}
    1.49  
    1.50  lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    1.51  nitpick [expect = genuine]
    1.52 @@ -82,7 +82,7 @@
    1.53  nitpick [card nat = 2, expect = none]
    1.54  oops
    1.55  
    1.56 -subsection {* 3.6. Inductive Datatypes *}
    1.57 +subsection {* 2.6. Inductive Datatypes *}
    1.58  
    1.59  lemma "hd (xs @ [y, y]) = hd xs"
    1.60  nitpick [expect = genuine]
    1.61 @@ -93,7 +93,7 @@
    1.62  nitpick [show_datatypes, expect = genuine]
    1.63  oops
    1.64  
    1.65 -subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
    1.66 +subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
    1.67  
    1.68  typedef three = "{0\<Colon>nat, 1, 2}"
    1.69  by blast
    1.70 @@ -148,7 +148,7 @@
    1.71  nitpick [show_datatypes, expect = genuine]
    1.72  oops
    1.73  
    1.74 -subsection {* 3.8. Inductive and Coinductive Predicates *}
    1.75 +subsection {* 2.8. Inductive and Coinductive Predicates *}
    1.76  
    1.77  inductive even where
    1.78  "even 0" |
    1.79 @@ -190,7 +190,7 @@
    1.80  nitpick [card nat = 10, show_consts, expect = genuine]
    1.81  oops
    1.82  
    1.83 -subsection {* 3.9. Coinductive Datatypes *}
    1.84 +subsection {* 2.9. Coinductive Datatypes *}
    1.85  
    1.86  (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
    1.87     we cannot rely on its presence, we expediently provide our own
    1.88 @@ -230,7 +230,7 @@
    1.89  nitpick [card = 1\<emdash>5, expect = none]
    1.90  sorry
    1.91  
    1.92 -subsection {* 3.10. Boxing *}
    1.93 +subsection {* 2.10. Boxing *}
    1.94  
    1.95  datatype tm = Var nat | Lam tm | App tm tm
    1.96  
    1.97 @@ -266,7 +266,7 @@
    1.98  nitpick [card = 1\<emdash>5, expect = none]
    1.99  sorry
   1.100  
   1.101 -subsection {* 3.11. Scope Monotonicity *}
   1.102 +subsection {* 2.11. Scope Monotonicity *}
   1.103  
   1.104  lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
   1.105  nitpick [verbose, expect = genuine]
   1.106 @@ -277,7 +277,7 @@
   1.107  nitpick [expect = genuine]
   1.108  oops
   1.109  
   1.110 -subsection {* 3.12. Inductive Properties *}
   1.111 +subsection {* 2.12. Inductive Properties *}
   1.112  
   1.113  inductive_set reach where
   1.114  "(4\<Colon>nat) \<in> reach" |
   1.115 @@ -340,11 +340,11 @@
   1.116    by auto
   1.117  qed
   1.118  
   1.119 -section {* 4. Case Studies *}
   1.120 +section {* 3. Case Studies *}
   1.121  
   1.122  nitpick_params [max_potential = 0]
   1.123  
   1.124 -subsection {* 4.1. A Context-Free Grammar *}
   1.125 +subsection {* 3.1. A Context-Free Grammar *}
   1.126  
   1.127  datatype alphabet = a | b
   1.128  
   1.129 @@ -418,7 +418,7 @@
   1.130  nitpick [card = 1\<emdash>5, expect = none]
   1.131  sorry
   1.132  
   1.133 -subsection {* 4.2. AA Trees *}
   1.134 +subsection {* 3.2. AA Trees *}
   1.135  
   1.136  datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
   1.137