--- 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 *}
--- a/src/HOL/Hilbert_Choice_lemmas.ML Wed Dec 05 03:06:05 2001 +0100
+++ b/src/HOL/Hilbert_Choice_lemmas.ML Wed Dec 05 03:07:44 2001 +0100
@@ -17,7 +17,6 @@
by (etac exE 1);
by (etac someI 1);
qed "someI_ex";
-AddXEs [someI_ex];
(*Easier to apply than someI: conclusion has only one occurrence of P*)
val prems = Goal "[| P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
--- a/src/ZF/Inductive.thy Wed Dec 05 03:06:05 2001 +0100
+++ b/src/ZF/Inductive.thy Wed Dec 05 03:07:44 2001 +0100
@@ -18,4 +18,11 @@
setup IndCases.setup
setup DatatypeTactics.setup
+
+(*belongs to theory ZF*)
+declare bspec [dest?]
+
+(*belongs to theory upair*)
+declare UnI1 [elim?] UnI2 [elim?]
+
end
--- a/src/ZF/ZF.ML Wed Dec 05 03:06:05 2001 +0100
+++ b/src/ZF/ZF.ML Wed Dec 05 03:07:44 2001 +0100
@@ -45,7 +45,6 @@
AddSIs [ballI];
AddEs [rev_ballE];
-AddXDs [bspec];
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
val ball_tac = dtac bspec THEN' assume_tac;
--- a/src/ZF/upair.ML Wed Dec 05 03:06:05 2001 +0100
+++ b/src/ZF/upair.ML Wed Dec 05 03:07:44 2001 +0100
@@ -84,7 +84,6 @@
AddSIs [UnCI];
AddSEs [UnE];
-AddXEs [UnI1, UnI2];
(*** Rules for small intersection -- Int -- defined via Upair ***)