--- 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