equal
deleted
inserted
replaced
28 val imp_le_cong = @{thm imp_le_cong}; |
28 val imp_le_cong = @{thm imp_le_cong}; |
29 val conj_le_cong = @{thm conj_le_cong}; |
29 val conj_le_cong = @{thm conj_le_cong}; |
30 val nat_mod_add_eq = @{thm mod_add1_eq} RS sym; |
30 val nat_mod_add_eq = @{thm mod_add1_eq} RS sym; |
31 val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym; |
31 val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym; |
32 val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym; |
32 val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym; |
33 val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym; |
33 val int_mod_add_eq = @{thm mod_add_eq} RS sym; |
34 val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym; |
34 val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym; |
35 val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym; |
35 val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym; |
36 val nat_div_add_eq = @{thm div_add1_eq} RS sym; |
36 val nat_div_add_eq = @{thm div_add1_eq} RS sym; |
37 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym; |
37 val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym; |
38 |
38 |