src/HOL/Integ/int_arith1.ML
changeset 18708 4b3dadb4fe33
parent 18328 841261f303a1
child 19044 d4bc0ee9383a
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -521,7 +521,7 @@
     1.4  in
     1.5  
     1.6  val int_arith_setup =
     1.7 - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.8 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.9     {add_mono_thms = add_mono_thms,
    1.10      mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
    1.11      inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
    1.12 @@ -529,10 +529,10 @@
    1.13      neqE = thm "linorder_neqE_int" :: neqE,
    1.14      simpset = simpset addsimps add_rules
    1.15                        addsimprocs simprocs
    1.16 -                      addcongs [if_weak_cong]}),
    1.17 -  arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT),
    1.18 -  arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT),
    1.19 -  arith_discrete "IntDef.int"];
    1.20 +                      addcongs [if_weak_cong]}) #>
    1.21 +  arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT) #>
    1.22 +  arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
    1.23 +  arith_discrete "IntDef.int";
    1.24  
    1.25  end;
    1.26