summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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