src/HOL/GCD.thy
changeset 56166 9a241bc276cd
parent 54867 c21a2465cac1
child 56218 1c3f1f2431f9
     1.1 --- a/src/HOL/GCD.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/GCD.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -1581,6 +1581,9 @@
     1.4    from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
     1.5  qed
     1.6  
     1.7 +declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
     1.8 +declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
     1.9 +
    1.10  lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
    1.11    by (fact Lcm_nat_empty)
    1.12  
    1.13 @@ -1736,11 +1739,11 @@
    1.14  
    1.15  lemma Lcm_set_int [code, code_unfold]:
    1.16    "Lcm (set xs) = fold lcm xs (1::int)"
    1.17 -  by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
    1.18 +  by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
    1.19  
    1.20  lemma Gcd_set_int [code, code_unfold]:
    1.21    "Gcd (set xs) = fold gcd xs (0::int)"
    1.22 -  by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)
    1.23 +  by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
    1.24  
    1.25  end
    1.26