src/HOL/GCD.thy
 changeset 44845 5e51075cbd97 parent 44821 a92f65e174cf child 44890 22f665a2e91c
```--- a/src/HOL/GCD.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/GCD.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -1463,17 +1463,17 @@
subsubsection {* The complete divisibility lattice *}

-interpretation gcd_semilattice_nat: semilattice_inf "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
+interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
proof
case goal3 thus ?case by(metis gcd_unique_nat)
qed auto

-interpretation lcm_semilattice_nat: semilattice_sup "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
+interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
proof
case goal3 thus ?case by(metis lcm_unique_nat)
qed auto

-interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
+interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..

text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
GCD is defined via LCM to facilitate the proof that we have a complete lattice.
@@ -1579,7 +1579,7 @@
qed

interpretation gcd_lcm_complete_lattice_nat:
-  complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
+  complete_lattice GCD LCM gcd "op dvd" "%m n::nat. m dvd n & ~ n dvd m" lcm 1 0
proof
case goal1 show ?case by simp
next```