equal
deleted
inserted
replaced
29 val mod_div_equality' = @{thm mod_div_equality'}; |
29 val mod_div_equality' = @{thm mod_div_equality'}; |
30 val split_div' = @{thm split_div'}; |
30 val split_div' = @{thm split_div'}; |
31 val Suc_plus1 = @{thm Suc_plus1}; |
31 val Suc_plus1 = @{thm Suc_plus1}; |
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; |
|
35 val mod_add_left_eq = @{thm mod_add_left_eq} RS sym; |
34 val mod_add_left_eq = @{thm mod_add_left_eq} RS sym; |
36 val mod_add_right_eq = @{thm mod_add_right_eq} RS sym; |
35 val mod_add_right_eq = @{thm mod_add_right_eq} RS sym; |
37 val int_mod_add_eq = @{thm mod_add_eq} RS sym; |
|
38 val nat_div_add_eq = @{thm div_add1_eq} RS sym; |
36 val nat_div_add_eq = @{thm div_add1_eq} RS sym; |
39 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym; |
37 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym; |
40 val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2; |
38 val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2; |
41 val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1; |
39 val ZDIVISION_BY_ZERO_DIV = @{thm DIVISION_BY_ZERO} RS conjunct1; |
42 |
40 |