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