equal
deleted
inserted
replaced
272 apply (drule hyperprime_factor_exists) |
272 apply (drule hyperprime_factor_exists) |
273 apply auto |
273 apply auto |
274 apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}") |
274 apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}") |
275 apply (force simp add: starprime_def, safe) |
275 apply (force simp add: starprime_def, safe) |
276 apply (drule_tac x = x in bspec, auto) |
276 apply (drule_tac x = x in bspec, auto) |
277 apply (metis add_commute hdvd_diff hdvd_one_eq_one hypnat_diff_add_inverse2 hypnat_one_not_prime) |
277 apply (metis add.commute hdvd_diff hdvd_one_eq_one hypnat_diff_add_inverse2 hypnat_one_not_prime) |
278 done |
278 done |
279 |
279 |
280 end |
280 end |