src/HOL/GCD.thy
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]