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]