--- 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"
--- 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