src/HOL/GCD.thy
 changeset 56218 1c3f1f2431f9 parent 56166 9a241bc276cd child 57512 cc97b347b301
```     1.1 --- a/src/HOL/GCD.thy	Wed Mar 19 17:06:02 2014 +0000
1.2 +++ b/src/HOL/GCD.thy	Wed Mar 19 18:47:22 2014 +0100
1.3 @@ -1558,8 +1558,8 @@
1.4  interpretation gcd_lcm_complete_lattice_nat:
1.5    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
1.6  where
1.7 -  "Inf.INFI Gcd A f = Gcd (f ` A :: nat set)"
1.8 -  and "Sup.SUPR Lcm A f = Lcm (f ` A)"
1.9 +  "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
1.10 +  and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
1.11  proof -
1.12    show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
1.13    proof
1.14 @@ -1577,8 +1577,8 @@
1.15    qed
1.16    then interpret gcd_lcm_complete_lattice_nat:
1.17      complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
1.18 -  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFI Gcd A f = Gcd (f ` A)" .
1.19 -  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
1.20 +  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
1.21 +  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" .
1.22  qed
1.23
1.24  declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
```