equal
deleted
inserted
replaced
148 apply (rule zcong_zless_imp_eq) |
148 apply (rule zcong_zless_imp_eq) |
149 apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *}) |
149 apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *}) |
150 apply (rule_tac [7] zcong_trans) |
150 apply (rule_tac [7] zcong_trans) |
151 apply (tactic {* stac (thm "zcong_sym") 8 *}) |
151 apply (tactic {* stac (thm "zcong_sym") 8 *}) |
152 apply (erule_tac [7] inv_is_inv) |
152 apply (erule_tac [7] inv_is_inv) |
153 apply (tactic "Asm_simp_tac 9") |
153 apply (tactic "asm_simp_tac @{simpset} 9") |
154 apply (erule_tac [9] inv_is_inv) |
154 apply (erule_tac [9] inv_is_inv) |
155 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
155 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
156 apply (rule_tac [8] inv_less) |
156 apply (rule_tac [8] inv_less) |
157 apply (rule_tac [7] inv_g_1 [THEN aux2]) |
157 apply (rule_tac [7] inv_g_1 [THEN aux2]) |
158 apply (unfold zprime_def) |
158 apply (unfold zprime_def) |