# HG changeset patch # User nipkow # Date 889605236 -3600 # Node ID b72dd6b2ba56d0e08989fd887baefc04296e9b85 # Parent b820f57a2323f4cd0b566b5b53d3dde9368a2486 New Asm_full_simp_tac led to a loop. diff -r b820f57a2323 -r b72dd6b2ba56 src/HOL/ex/Primes.ML --- a/src/HOL/ex/Primes.ML Tue Mar 10 20:24:28 1998 +0100 +++ b/src/HOL/ex/Primes.ML Wed Mar 11 09:33:56 1998 +0100 @@ -79,10 +79,10 @@ goal thy "k * gcd(m,n) = gcd(k*m, k*n)"; by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1); by (case_tac "k=0" 1); -by (case_tac "n=0" 2); -by (ALLGOALS - (asm_full_simp_tac (simpset() addsimps - [mod_less_divisor, mod_geq, mod_mult_distrib2]))); + by(Asm_full_simp_tac 1); +by (case_tac "n=0" 1); + by(Asm_full_simp_tac 1); +by(asm_full_simp_tac (simpset() addsimps [mod_geq, mod_mult_distrib2]) 1); qed "gcd_mult_distrib2"; (*This theorem leads immediately to a proof of the uniqueness of factorization.