src/HOL/Meson.thy
 changeset 40620 7a9278de19ad parent 39953 aa54f347e5e2 child 42616 92715b528e78
```     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"
```