src/HOL/GCD.thy
changeset 61566 c3d6e570ccef
parent 61169 4de9ff3ea29a
child 61605 1bf7b186542e
     1.1 --- a/src/HOL/GCD.thy	Wed Nov 04 08:13:49 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Wed Nov 04 08:13:52 2015 +0100
     1.3 @@ -1971,7 +1971,7 @@
     1.4  
     1.5  interpretation gcd_lcm_complete_lattice_nat:
     1.6    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
     1.7 -where "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
     1.8 +rewrites "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
     1.9    and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
    1.10  proof -
    1.11    show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"