src/HOL/GCD.thy
 changeset 54257 5c7a3b6b05a9 parent 52729 412c9e0381a1 child 54437 0060957404c7
```--- a/src/HOL/GCD.thy	Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/GCD.thy	Tue Nov 05 09:44:57 2013 +0100
@@ -1555,8 +1555,8 @@
interpretation gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
where
-  "complete_lattice.INFI Gcd A f = Gcd (f ` A :: nat set)"
-  and "complete_lattice.SUPR Lcm A f = Lcm (f ` A)"
+  "Inf.INFI Gcd A f = Gcd (f ` A :: nat set)"
+  and "Sup.SUPR Lcm A f = Lcm (f ` A)"
proof -
show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
proof
@@ -1574,8 +1574,8 @@
qed
then interpret gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
-  from gcd_lcm_complete_lattice_nat.INF_def show "complete_lattice.INFI Gcd A f = Gcd (f ` A)" .
-  from gcd_lcm_complete_lattice_nat.SUP_def show "complete_lattice.SUPR Lcm A f = Lcm (f ` A)" .
+  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFI Gcd A f = Gcd (f ` A)" .
+  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
qed

lemma Lcm_empty_nat: "Lcm {} = (1::nat)"```