equal
deleted
inserted
replaced
82 apply (case_tac "n=0") |
82 apply (case_tac "n=0") |
83 apply (simp_all add: dvd_mod); |
83 apply (simp_all add: dvd_mod); |
84 done; |
84 done; |
85 |
85 |
86 theorem gcd_greatest_iff [iff]: |
86 theorem gcd_greatest_iff [iff]: |
87 "k dvd gcd(m,n) = (k dvd m \<and> k dvd n)" |
87 "(k dvd gcd(m,n)) = (k dvd m \<and> k dvd n)" |
88 apply (blast intro!: gcd_greatest intro: dvd_trans); |
88 apply (blast intro!: gcd_greatest intro: dvd_trans); |
89 done; |
89 done; |
90 |
90 |
91 |
91 |
92 constdefs |
92 constdefs |