equal
deleted
inserted
replaced
906 by (subgoal_tac "(#-1 + - (#2 * b)) = - (#1 + (#2 * b))" 1); |
906 by (subgoal_tac "(#-1 + - (#2 * b)) = - (#1 + (#2 * b))" 1); |
907 by (Simp_tac 2); |
907 by (Simp_tac 2); |
908 by (asm_full_simp_tac (HOL_ss |
908 by (asm_full_simp_tac (HOL_ss |
909 addsimps [zmod_zminus_zminus, zdiff_def, |
909 addsimps [zmod_zminus_zminus, zdiff_def, |
910 zminus_zadd_distrib RS sym]) 1); |
910 zminus_zadd_distrib RS sym]) 1); |
911 bd (zminus_equation RS iffD1 RS sym) 1; |
911 by (dtac (zminus_equation RS iffD1 RS sym) 1); |
912 by (auto_tac (claset(), |
912 by (auto_tac (claset(), |
913 simpset() addsimps [zmult_zminus_right])); |
913 simpset() addsimps [zmult_zminus_right])); |
914 qed "neg_zmod_times_2"; |
914 qed "neg_zmod_times_2"; |
915 |
915 |
916 Goal "number_of (v BIT b) mod number_of (w BIT False) = \ |
916 Goal "number_of (v BIT b) mod number_of (w BIT False) = \ |