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"