src/HOL/NumberTheory/Chinese.ML
changeset 10175 76646fc8b1bf
parent 9943 55c82decf3f4
child 10658 b9d43a2add79
equal deleted inserted replaced
10174:ba7955d211c4 10175:76646fc8b1bf
   208 \                [(kf i)*(mhf mf n i)*(xilin_sol i n kf bf mf) = bf i] \
   208 \                [(kf i)*(mhf mf n i)*(xilin_sol i n kf bf mf) = bf i] \
   209 \                  (mod mf i)" 7);
   209 \                  (mod mf i)" 7);
   210 by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
   210 by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
   211 by (rewtac xilin_sol_def);
   211 by (rewtac xilin_sol_def);
   212 by (Asm_simp_tac 7);
   212 by (Asm_simp_tac 7);
   213 by (rtac (ex1_implies_ex RS ex_someI) 7);
   213 by (rtac (ex1_implies_ex RS someI_ex) 7);
   214 by (rtac unique_xi_sol 7);
   214 by (rtac unique_xi_sol 7);
   215 by (rtac funprod_zdvd 4);
   215 by (rtac funprod_zdvd 4);
   216 by (rewtac m_cond_def);
   216 by (rewtac m_cond_def);
   217 by (rtac (funprod_pos RS pos_mod_sign) 1);
   217 by (rtac (funprod_pos RS pos_mod_sign) 1);
   218 by (rtac (funprod_pos RS pos_mod_bound) 2);
   218 by (rtac (funprod_pos RS pos_mod_bound) 2);