equal
deleted
inserted
replaced
1000 apply (unfold word_size) |
1000 apply (unfold word_size) |
1001 apply (simp add: un_ui_le) |
1001 apply (simp add: un_ui_le) |
1002 apply (auto simp add: unat_def uint_sub_if') |
1002 apply (auto simp add: unat_def uint_sub_if') |
1003 apply (rule nat_diff_distrib) |
1003 apply (rule nat_diff_distrib) |
1004 prefer 3 |
1004 prefer 3 |
1005 apply (simp add: group_simps) |
1005 apply (simp add: algebra_simps) |
1006 apply (rule nat_diff_distrib [THEN trans]) |
1006 apply (rule nat_diff_distrib [THEN trans]) |
1007 prefer 3 |
1007 prefer 3 |
1008 apply (subst nat_add_distrib) |
1008 apply (subst nat_add_distrib) |
1009 prefer 3 |
1009 prefer 3 |
1010 apply (simp add: nat_power_eq) |
1010 apply (simp add: nat_power_eq) |