equal
deleted
inserted
replaced
166 by (Asm_simp_tac 2); |
166 by (Asm_simp_tac 2); |
167 by (dtac (int_0_less_mult_iff RS iffD1) 1); |
167 by (dtac (int_0_less_mult_iff RS iffD1) 1); |
168 by Auto_tac; |
168 by Auto_tac; |
169 qed "pos_zmult_eq_1_iff"; |
169 qed "pos_zmult_eq_1_iff"; |
170 |
170 |
171 Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = # -1 & n = # -1))"; |
171 Goal "(m*n = (Numeral1::int)) = ((m = Numeral1 & n = Numeral1) | (m = -1 & n = -1))"; |
172 by (case_tac "Numeral0<m" 1); |
172 by (case_tac "Numeral0<m" 1); |
173 by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1); |
173 by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1); |
174 by (case_tac "m=Numeral0" 1); |
174 by (case_tac "m=Numeral0" 1); |
175 by (Asm_simp_tac 1); |
175 by (Asm_simp_tac 1); |
176 by (subgoal_tac "Numeral0 < -m" 1); |
176 by (subgoal_tac "Numeral0 < -m" 1); |