tuned declarations;
authorwenzelm
Wed Dec 05 03:07:44 2001 +0100 (2001-12-05)
changeset 12372cd3a09c7dac9
parent 12371 80ca9058db95
child 12373 704e50ab65af
tuned declarations;
src/HOL/Hilbert_Choice.thy
src/HOL/Hilbert_Choice_lemmas.ML
src/ZF/Inductive.thy
src/ZF/ZF.ML
src/ZF/upair.ML
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Dec 05 03:06:05 2001 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Dec 05 03:07:44 2001 +0100
     1.3 @@ -37,6 +37,8 @@
     1.4  
     1.5  
     1.6  use "Hilbert_Choice_lemmas.ML"
     1.7 +declare someI_ex [elim?];
     1.8 +
     1.9  
    1.10  lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    1.11    -- {* dynamically-scoped fact for TFL *}
     2.1 --- a/src/HOL/Hilbert_Choice_lemmas.ML	Wed Dec 05 03:06:05 2001 +0100
     2.2 +++ b/src/HOL/Hilbert_Choice_lemmas.ML	Wed Dec 05 03:07:44 2001 +0100
     2.3 @@ -17,7 +17,6 @@
     2.4  by (etac exE 1);
     2.5  by (etac someI 1);
     2.6  qed "someI_ex";
     2.7 -AddXEs [someI_ex];
     2.8  
     2.9  (*Easier to apply than someI: conclusion has only one occurrence of P*)
    2.10  val prems = Goal "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
     3.1 --- a/src/ZF/Inductive.thy	Wed Dec 05 03:06:05 2001 +0100
     3.2 +++ b/src/ZF/Inductive.thy	Wed Dec 05 03:07:44 2001 +0100
     3.3 @@ -18,4 +18,11 @@
     3.4  setup IndCases.setup
     3.5  setup DatatypeTactics.setup
     3.6  
     3.7 +
     3.8 +(*belongs to theory ZF*)
     3.9 +declare bspec [dest?]
    3.10 +
    3.11 +(*belongs to theory upair*)
    3.12 +declare UnI1 [elim?]  UnI2 [elim?]
    3.13 +
    3.14  end
     4.1 --- a/src/ZF/ZF.ML	Wed Dec 05 03:06:05 2001 +0100
     4.2 +++ b/src/ZF/ZF.ML	Wed Dec 05 03:07:44 2001 +0100
     4.3 @@ -45,7 +45,6 @@
     4.4  
     4.5  AddSIs [ballI];
     4.6  AddEs  [rev_ballE];
     4.7 -AddXDs [bspec];
     4.8  
     4.9  (*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
    4.10  val ball_tac = dtac bspec THEN' assume_tac;
     5.1 --- a/src/ZF/upair.ML	Wed Dec 05 03:06:05 2001 +0100
     5.2 +++ b/src/ZF/upair.ML	Wed Dec 05 03:07:44 2001 +0100
     5.3 @@ -84,7 +84,6 @@
     5.4  
     5.5  AddSIs [UnCI];
     5.6  AddSEs [UnE];
     5.7 -AddXEs [UnI1, UnI2];
     5.8  
     5.9  
    5.10  (*** Rules for small intersection -- Int -- defined via Upair ***)