src/HOL/GCD.thy
changeset 62349 7c23469b5118
parent 62348 9a5f43dac883
child 62350 66a381d3f88f
     1.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -2167,24 +2167,4 @@
     1.4  lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
     1.5    by (fact dvd_gcdD2)
     1.6  
     1.7 -interpretation dvd:
     1.8 -  order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
     1.9 -  by standard (auto intro: dvd_refl dvd_trans dvd_antisym)
    1.10 -
    1.11 -interpretation gcd_semilattice_nat:
    1.12 -  semilattice_inf gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
    1.13 -  by standard (auto dest: dvd_antisym dvd_trans)
    1.14 -
    1.15 -interpretation lcm_semilattice_nat:
    1.16 -  semilattice_sup lcm Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
    1.17 -  by standard simp_all
    1.18 -
    1.19 -interpretation gcd_lcm_lattice_nat:
    1.20 -  lattice gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n" lcm
    1.21 -  ..
    1.22 -
    1.23 -interpretation gcd_lcm_complete_lattice_nat:
    1.24 -  complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n" lcm 1 "0::nat"
    1.25 -  by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
    1.26 -
    1.27  end