src/HOL/Decision_Procs/ferrack_tac.ML
changeset 29948 cdf12a1cb963
parent 29823 0ab754d13ccd
child 30034 60f64f112174
child 30240 5b25fee0362c
equal deleted inserted replaced
29947:0a51765d2084 29948:cdf12a1cb963
    32 val imp_le_cong = @{thm imp_le_cong};
    32 val imp_le_cong = @{thm imp_le_cong};
    33 val conj_le_cong = @{thm conj_le_cong};
    33 val conj_le_cong = @{thm conj_le_cong};
    34 val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
    34 val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
    35 val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    35 val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    36 val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    36 val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    37 val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
    37 val int_mod_add_eq = @{thm mod_add_eq} RS sym;
    38 val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
    38 val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
    39 val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
    39 val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
    40 val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    40 val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    41 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    41 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    42 val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
    42 val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;