src/HOL/Hilbert_Choice.thy
changeset 17893 aef5a6d11c2a
parent 17702 ea88ddeafabe
child 18389 8352b1d3b639
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Oct 18 17:59:25 2005 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Oct 18 17:59:26 2005 +0200
     1.3 @@ -493,7 +493,6 @@
     1.4  
     1.5  subsection{*Lemmas for Meson, the Model Elimination Procedure*}
     1.6  
     1.7 -
     1.8  text{* Generation of contrapositives *}
     1.9  
    1.10  text{*Inserts negated disjunct after removing the negation; P is a literal.
    1.11 @@ -620,9 +619,17 @@
    1.12  *}
    1.13  
    1.14  
    1.15 +subsection {* Meson method setup *}
    1.16 +
    1.17  use "Tools/meson.ML"
    1.18  setup Meson.skolemize_setup
    1.19  
    1.20 +
    1.21 +subsection {* Specification package -- Hilbertized version *}
    1.22 +
    1.23 +lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
    1.24 +  by (simp only: someI_ex)
    1.25 +
    1.26  use "Tools/specification_package.ML"
    1.27  
    1.28  end