equal
deleted
inserted
replaced
49 lemmas compute_div_mod = div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1 |
49 lemmas compute_div_mod = div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1 |
50 one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral |
50 one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral |
51 one_div_minus_numeral one_mod_minus_numeral |
51 one_div_minus_numeral one_mod_minus_numeral |
52 numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral |
52 numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral |
53 numeral_div_minus_numeral numeral_mod_minus_numeral |
53 numeral_div_minus_numeral numeral_mod_minus_numeral |
54 div_minus_minus mod_minus_minus adjust_div_eq of_bool_eq one_neq_zero |
54 div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero |
55 numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial |
55 numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial |
56 divmod_steps divmod_cancel divmod_step_eq fst_conv snd_conv numeral_One |
56 divmod_steps divmod_cancel divmod_step_eq fst_conv snd_conv numeral_One |
57 case_prod_beta rel_simps adjust_mod_def div_minus1_right mod_minus1_right |
57 case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right |
58 minus_minus numeral_times_numeral mult_zero_right mult_1_right |
58 minus_minus numeral_times_numeral mult_zero_right mult_1_right |
59 |
59 |
60 |
60 |
61 (* collecting all the theorems *) |
61 (* collecting all the theorems *) |
62 |
62 |