| changeset 62347 | 2230b7047376 |
| parent 62346 | 97f2ed240431 |
| child 62348 | 9a5f43dac883 |
--- a/src/HOL/GCD.thy Wed Feb 17 21:51:56 2016 +0100 +++ b/src/HOL/GCD.thy Wed Feb 17 21:51:57 2016 +0100 @@ -2057,9 +2057,6 @@ text \<open>Fact aliasses\<close> -lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>" - by (fact dvd_int_unfold_dvd_nat) - lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat] lemmas gcd_assoc_int = gcd.assoc [where ?'a = int] lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]