src/HOL/ex/Primes.thy
changeset 9941 fe05af7ec816
parent 9912 4b02467a4412
     1.1 --- a/src/HOL/ex/Primes.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/ex/Primes.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5  (*Maximality: for all m,n,k naturals, 
     1.6                  if k divides m and k divides n then k divides gcd(m,n)*)
     1.7 -lemma gcd_greatest [rulified]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
     1.8 +lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
     1.9    apply (induct_tac m n rule: gcd_induct)
    1.10    apply (simp_all add: gcd_non_0 dvd_mod);
    1.11    done;