equal
deleted
inserted
replaced
97 \ ==> [x=y] (mod mf n)"; |
97 \ ==> [x=y] (mod mf n)"; |
98 by (rtac iffD1 1); |
98 by (rtac iffD1 1); |
99 by (res_inst_tac [("k","kf n")] zcong_cancel2 1); |
99 by (res_inst_tac [("k","kf n")] zcong_cancel2 1); |
100 by (res_inst_tac [("b","bf n")] zcong_trans 3); |
100 by (res_inst_tac [("b","bf n")] zcong_trans 3); |
101 by (stac zcong_sym 4); |
101 by (stac zcong_sym 4); |
102 by (rtac zless_imp_zle 1); |
102 by (rtac order_less_imp_le 1); |
103 by (ALLGOALS Asm_simp_tac); |
103 by (ALLGOALS Asm_simp_tac); |
104 val lemma = result(); |
104 val lemma = result(); |
105 |
105 |
106 Goal "m_cond n mf --> km_cond n kf mf --> \ |
106 Goal "m_cond n mf --> km_cond n kf mf --> \ |
107 \ lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y --> \ |
107 \ lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y --> \ |