src/HOL/GCD.thy
changeset 61169 4de9ff3ea29a
parent 60758 d8d85a8172b5
child 61566 c3d6e570ccef
     1.1 --- a/src/HOL/GCD.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -1975,7 +1975,7 @@
     1.4    and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
     1.5  proof -
     1.6    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.7 -    by default (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
     1.8 +    by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
     1.9    then interpret gcd_lcm_complete_lattice_nat:
    1.10      complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
    1.11    from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .