tuned declaration of rules;
authorwenzelm
Sun Oct 28 21:14:56 2001 +0100 (2001-10-28)
changeset 119772e7c54b86763
parent 11976 075df6e46cef
child 11978 a394d3e9c8bb
tuned declaration of rules;
src/HOL/HOL.ML
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.ML	Sun Oct 28 21:10:47 2001 +0100
     1.2 +++ b/src/HOL/HOL.ML	Sun Oct 28 21:14:56 2001 +0100
     1.3 @@ -29,9 +29,6 @@
     1.4    val arbitrary_def = arbitrary_def;
     1.5  end;
     1.6  
     1.7 -AddXIs [equal_intr_rule, ext];
     1.8 -AddXEs [disjI1, disjI2, ex1_implies_ex, sym];
     1.9 -
    1.10  open HOL;
    1.11  
    1.12  val Least_def = thm "Least_def";
     2.1 --- a/src/HOL/HOL.thy	Sun Oct 28 21:10:47 2001 +0100
     2.2 +++ b/src/HOL/HOL.thy	Sun Oct 28 21:14:56 2001 +0100
     2.3 @@ -252,10 +252,15 @@
     2.4  
     2.5  use "cladata.ML"
     2.6  setup hypsubst_setup
     2.7 +
     2.8  declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
     2.9 +
    2.10  setup Classical.setup
    2.11  setup clasetup
    2.12  
    2.13 +declare ext [intro?]
    2.14 +declare disjI1 [elim?]  disjI2 [elim?]  ex1_implies_ex [elim?]  sym [elim?]
    2.15 +
    2.16  use "blastdata.ML"
    2.17  setup Blast.setup
    2.18