# 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 \ Q \ Trueprop P \ Trueprop Q" by simp @@ -174,7 +174,7 @@ done -section {* Skolemization helpers *} +subsection {* Skolemization helpers *} definition skolem :: "'a \ 'a" where [no_atp]: "skolem = (\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 \ term list option) \ code_numeral \ 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