# HG changeset patch
# User wenzelm
# Date 1007518064 -3600
# Node ID cd3a09c7dac9f7a29efef7037d5ec1b386cabf65
# Parent  80ca9058db95693a03a8502066541e0739b43d2f
tuned declarations;

diff -r 80ca9058db95 -r cd3a09c7dac9 src/HOL/Hilbert_Choice.thy
--- 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 *}
diff -r 80ca9058db95 -r cd3a09c7dac9 src/HOL/Hilbert_Choice_lemmas.ML
--- 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)";
diff -r 80ca9058db95 -r cd3a09c7dac9 src/ZF/Inductive.thy
--- 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
diff -r 80ca9058db95 -r cd3a09c7dac9 src/ZF/ZF.ML
--- 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;
diff -r 80ca9058db95 -r cd3a09c7dac9 src/ZF/upair.ML
--- 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 ***)