eliminated technical fact alias
authorhaftmann
Wed Feb 18 22:46:48 2015 +0100 (2015-02-18)
changeset 59556aa2deef7cf47
parent 59555 05573e5504a9
child 59557 ebd8ecacfba6
eliminated technical fact alias
src/HOL/Divides.thy
src/HOL/Int.thy
src/HOL/Tools/numeral_simprocs.ML
     1.1 --- a/src/HOL/Divides.thy	Wed Feb 18 22:46:48 2015 +0100
     1.2 +++ b/src/HOL/Divides.thy	Wed Feb 18 22:46:48 2015 +0100
     1.3 @@ -1914,9 +1914,6 @@
     1.4  
     1.5  text {* Tool setup *}
     1.6  
     1.7 -(* FIXME: Theorem list add_0s doesn't exist, because Numeral0 has gone. *)
     1.8 -lemmas add_0s = add_0_left add_0_right
     1.9 -
    1.10  ML {*
    1.11  structure Cancel_Div_Mod_Int = Cancel_Div_Mod
    1.12  (
    1.13 @@ -1929,7 +1926,7 @@
    1.14    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
    1.15  
    1.16    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
    1.17 -    (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms ac_simps}))
    1.18 +    (@{thm diff_conv_add_uminus} :: @{thms add_0_left add_0_right} @ @{thms ac_simps}))
    1.19  )
    1.20  *}
    1.21  
     2.1 --- a/src/HOL/Int.thy	Wed Feb 18 22:46:48 2015 +0100
     2.2 +++ b/src/HOL/Int.thy	Wed Feb 18 22:46:48 2015 +0100
     2.3 @@ -747,9 +747,6 @@
     2.4  lemmas of_int_simps =
     2.5    of_int_0 of_int_1 of_int_add of_int_mult
     2.6  
     2.7 -lemmas int_arith_rules =
     2.8 -  numeral_One more_arith_simps of_nat_simps of_int_simps
     2.9 -
    2.10  ML_file "Tools/int_arith.ML"
    2.11  declaration {* K Int_Arith.setup *}
    2.12  
     3.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 18 22:46:48 2015 +0100
     3.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 18 22:46:48 2015 +0100
     3.3 @@ -177,7 +177,7 @@
     3.4  val numeral_syms = [@{thm numeral_1_eq_1} RS sym];
     3.5  
     3.6  (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
     3.7 -val add_0s =  @{thms add_0s};
     3.8 +val add_0s =  @{thms add_0_left add_0_right};
     3.9  val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right divide_1};
    3.10  
    3.11  (* For post-simplification of the rhs of simproc-generated rules *)