src/HOL/GCD.thy
changeset 44845 5e51075cbd97
parent 44821 a92f65e174cf
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/GCD.thy	Thu Sep 08 08:41:28 2011 -0700
     1.2 +++ b/src/HOL/GCD.thy	Fri Sep 09 00:22:18 2011 +0200
     1.3 @@ -1463,17 +1463,17 @@
     1.4  subsubsection {* The complete divisibility lattice *}
     1.5  
     1.6  
     1.7 -interpretation gcd_semilattice_nat: semilattice_inf "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
     1.8 +interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
     1.9  proof
    1.10    case goal3 thus ?case by(metis gcd_unique_nat)
    1.11  qed auto
    1.12  
    1.13 -interpretation lcm_semilattice_nat: semilattice_sup "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
    1.14 +interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
    1.15  proof
    1.16    case goal3 thus ?case by(metis lcm_unique_nat)
    1.17  qed auto
    1.18  
    1.19 -interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
    1.20 +interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..
    1.21  
    1.22  text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
    1.23  GCD is defined via LCM to facilitate the proof that we have a complete lattice.
    1.24 @@ -1579,7 +1579,7 @@
    1.25  qed
    1.26  
    1.27  interpretation gcd_lcm_complete_lattice_nat:
    1.28 -  complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
    1.29 +  complete_lattice GCD LCM gcd "op dvd" "%m n::nat. m dvd n & ~ n dvd m" lcm 1 0
    1.30  proof
    1.31    case goal1 show ?case by simp
    1.32  next