# HG changeset patch
# User huffman
# Date 1290022784 28800
# Node ID 7a9278de19ad5d83acaca48df52545576c15054a
# Parent  84edf7177d737d64a55f8f7b6f7856a85f0a1ac1
section -> subsection

diff -r 84edf7177d73 -r 7a9278de19ad src/HOL/Meson.thy
--- a/src/HOL/Meson.thy	Wed Nov 17 11:07:02 2010 -0800
+++ b/src/HOL/Meson.thy	Wed Nov 17 11:39:44 2010 -0800
@@ -14,7 +14,7 @@
      ("Tools/Meson/meson_tactic.ML")
 begin
 
-section {* Negation Normal Form *}
+subsection {* Negation Normal Form *}
 
 text {* de Morgan laws *}
 
@@ -37,7 +37,7 @@
   by fast+
 
 
-section {* Pulling out the existential quantifiers *}
+subsection {* Pulling out the existential quantifiers *}
 
 text {* Conjunction *}
 
@@ -95,7 +95,7 @@
 by blast
 
 
-section {* Lemmas for Forward Proof *}
+subsection {* Lemmas for Forward Proof *}
 
 text{*There is a similarity to congruence rules*}
 
@@ -120,7 +120,7 @@
 by blast
 
 
-section {* Clausification helper *}
+subsection {* Clausification helper *}
 
 lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
 by simp
@@ -174,7 +174,7 @@
 done
 
 
-section {* Skolemization helpers *}
+subsection {* Skolemization helpers *}
 
 definition skolem :: "'a \<Rightarrow> 'a" where
 [no_atp]: "skolem = (\<lambda>x. x)"
@@ -186,7 +186,7 @@
 lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
 
 
-section {* Meson package *}
+subsection {* Meson package *}
 
 use "Tools/Meson/meson.ML"
 use "Tools/Meson/meson_clausify.ML"
diff -r 84edf7177d73 -r 7a9278de19ad src/HOL/Smallcheck.thy
--- a/src/HOL/Smallcheck.thy	Wed Nov 17 11:07:02 2010 -0800
+++ b/src/HOL/Smallcheck.thy	Wed Nov 17 11:39:44 2010 -0800
@@ -8,7 +8,7 @@
 begin
 
 
-section {* small value generator type classes *}
+subsection {* small value generator type classes *}
 
 class small = term_of +
 fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
@@ -48,7 +48,7 @@
 
 end
 
-section {* Defining combinators for any first-order data type *}
+subsection {* Defining combinators for any first-order data type *}
 
 definition catch_match :: "term list option => term list option => term list option"
 where