src/HOL/Hilbert_Choice.thy
changeset 12372 cd3a09c7dac9
parent 12298 b344486c33e2
child 13585 db4005b40cc6
--- 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 *}