section -> subsection
authorhuffman
Wed Nov 17 11:39:44 2010 -0800 (2010-11-17)
changeset 406207a9278de19ad
parent 40619 84edf7177d73
child 40621 86f598f84188
section -> subsection
src/HOL/Meson.thy
src/HOL/Smallcheck.thy
     1.1 --- a/src/HOL/Meson.thy	Wed Nov 17 11:07:02 2010 -0800
     1.2 +++ b/src/HOL/Meson.thy	Wed Nov 17 11:39:44 2010 -0800
     1.3 @@ -14,7 +14,7 @@
     1.4       ("Tools/Meson/meson_tactic.ML")
     1.5  begin
     1.6  
     1.7 -section {* Negation Normal Form *}
     1.8 +subsection {* Negation Normal Form *}
     1.9  
    1.10  text {* de Morgan laws *}
    1.11  
    1.12 @@ -37,7 +37,7 @@
    1.13    by fast+
    1.14  
    1.15  
    1.16 -section {* Pulling out the existential quantifiers *}
    1.17 +subsection {* Pulling out the existential quantifiers *}
    1.18  
    1.19  text {* Conjunction *}
    1.20  
    1.21 @@ -95,7 +95,7 @@
    1.22  by blast
    1.23  
    1.24  
    1.25 -section {* Lemmas for Forward Proof *}
    1.26 +subsection {* Lemmas for Forward Proof *}
    1.27  
    1.28  text{*There is a similarity to congruence rules*}
    1.29  
    1.30 @@ -120,7 +120,7 @@
    1.31  by blast
    1.32  
    1.33  
    1.34 -section {* Clausification helper *}
    1.35 +subsection {* Clausification helper *}
    1.36  
    1.37  lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
    1.38  by simp
    1.39 @@ -174,7 +174,7 @@
    1.40  done
    1.41  
    1.42  
    1.43 -section {* Skolemization helpers *}
    1.44 +subsection {* Skolemization helpers *}
    1.45  
    1.46  definition skolem :: "'a \<Rightarrow> 'a" where
    1.47  [no_atp]: "skolem = (\<lambda>x. x)"
    1.48 @@ -186,7 +186,7 @@
    1.49  lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
    1.50  
    1.51  
    1.52 -section {* Meson package *}
    1.53 +subsection {* Meson package *}
    1.54  
    1.55  use "Tools/Meson/meson.ML"
    1.56  use "Tools/Meson/meson_clausify.ML"
     2.1 --- a/src/HOL/Smallcheck.thy	Wed Nov 17 11:07:02 2010 -0800
     2.2 +++ b/src/HOL/Smallcheck.thy	Wed Nov 17 11:39:44 2010 -0800
     2.3 @@ -8,7 +8,7 @@
     2.4  begin
     2.5  
     2.6  
     2.7 -section {* small value generator type classes *}
     2.8 +subsection {* small value generator type classes *}
     2.9  
    2.10  class small = term_of +
    2.11  fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    2.12 @@ -48,7 +48,7 @@
    2.13  
    2.14  end
    2.15  
    2.16 -section {* Defining combinators for any first-order data type *}
    2.17 +subsection {* Defining combinators for any first-order data type *}
    2.18  
    2.19  definition catch_match :: "term list option => term list option => term list option"
    2.20  where