added lemma exE_some (from specification_package.ML);
authorwenzelm
Tue Oct 18 17:59:26 2005 +0200 (2005-10-18)
changeset 17893aef5a6d11c2a
parent 17892 62c397c17d18
child 17894 f2fdd22accaa
added lemma exE_some (from specification_package.ML);
src/HOL/Hilbert_Choice.thy
     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