# HG changeset patch
# User wenzelm
# Date 1129651166 -7200
# Node ID aef5a6d11c2ae483baf91b14da824e2b116372a1
# Parent  62c397c17d18a170a0f12eb5d2086062eaef2b74
added lemma exE_some (from specification_package.ML);

diff -r 62c397c17d18 -r aef5a6d11c2a src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Tue Oct 18 17:59:25 2005 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Tue Oct 18 17:59:26 2005 +0200
@@ -493,7 +493,6 @@
 
 subsection{*Lemmas for Meson, the Model Elimination Procedure*}
 
-
 text{* Generation of contrapositives *}
 
 text{*Inserts negated disjunct after removing the negation; P is a literal.
@@ -620,9 +619,17 @@
 *}
 
 
+subsection {* Meson method setup *}
+
 use "Tools/meson.ML"
 setup Meson.skolemize_setup
 
+
+subsection {* Specification package -- Hilbertized version *}
+
+lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
+  by (simp only: someI_ex)
+
 use "Tools/specification_package.ML"
 
 end