equal
deleted
inserted
replaced
197 by (full_simp_tac (simpset() addsimps [pideal_structure]) 1); |
197 by (full_simp_tac (simpset() addsimps [pideal_structure]) 1); |
198 qed "in_pideal_imp_dvd"; |
198 qed "in_pideal_imp_dvd"; |
199 |
199 |
200 Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"; |
200 Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"; |
201 by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1); |
201 by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1); |
202 by (simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); |
202 by (etac contrapos_pp 1); |
203 by (etac contrapos 1); |
203 by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); |
204 by (rtac in_pideal_imp_dvd 1); |
204 by (rtac in_pideal_imp_dvd 1); |
205 by (Asm_simp_tac 1); |
205 by (Asm_simp_tac 1); |
206 by (res_inst_tac [("x", "<0>")] exI 1); |
206 by (res_inst_tac [("x", "<0>")] exI 1); |
207 by (res_inst_tac [("x", "<1>")] exI 1); |
207 by (res_inst_tac [("x", "<1>")] exI 1); |
208 by (Simp_tac 1); |
208 by (Simp_tac 1); |