--- a/src/HOL/Hilbert_Choice.thy Wed Dec 05 03:06:05 2001 +0100
+++ b/src/HOL/Hilbert_Choice.thy Wed Dec 05 03:07:44 2001 +0100
@@ -37,6 +37,8 @@
use "Hilbert_Choice_lemmas.ML"
+declare someI_ex [elim?];
+
lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
-- {* dynamically-scoped fact for TFL *}