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