src/HOL/Decision_Procs/ferrack_tac.ML
changeset 30224 79136ce06bdb
parent 30034 60f64f112174
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -31,10 +31,8 @@
     1.4  val Suc_plus1 = @{thm Suc_plus1};
     1.5  val imp_le_cong = @{thm imp_le_cong};
     1.6  val conj_le_cong = @{thm conj_le_cong};
     1.7 -val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
     1.8  val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
     1.9  val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    1.10 -val int_mod_add_eq = @{thm mod_add_eq} RS sym;
    1.11  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    1.12  val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    1.13  val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;