src/HOL/GCD.thy
changeset 59667 651ea265d568
parent 59545 12a6088ed195
child 59807 22bc39064290
     1.1 --- a/src/HOL/GCD.thy	Tue Mar 10 11:56:32 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Tue Mar 10 15:20:40 2015 +0000
     1.3 @@ -28,7 +28,7 @@
     1.4  section {* Greatest common divisor and least common multiple *}
     1.5  
     1.6  theory GCD
     1.7 -imports Fact
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  declare One_nat_def [simp del]
    1.12 @@ -50,7 +50,7 @@
    1.13  class semiring_gcd = comm_semiring_1 + gcd +
    1.14    assumes gcd_dvd1 [iff]: "gcd a b dvd a"
    1.15  		and gcd_dvd2 [iff]: "gcd a b dvd b"
    1.16 -		and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 
    1.17 +		and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
    1.18  
    1.19  class ring_gcd = comm_ring_1 + semiring_gcd
    1.20  
    1.21 @@ -266,10 +266,10 @@
    1.22    then show "k dvd gcd m n"
    1.23      by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
    1.24  qed
    1.25 -  
    1.26 +
    1.27  instance int :: ring_gcd
    1.28    by intro_classes (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def gcd_greatest)
    1.29 -  
    1.30 +
    1.31  lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
    1.32    by (metis gcd_dvd1 dvd_trans)
    1.33  
    1.34 @@ -1753,12 +1753,12 @@
    1.35  
    1.36  
    1.37  text \<open>Fact aliasses\<close>
    1.38 -  
    1.39 -lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat] 
    1.40 +
    1.41 +lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
    1.42    and gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
    1.43    and gcd_greatest_nat = gcd_greatest [where ?'a = nat]
    1.44  
    1.45 -lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int] 
    1.46 +lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
    1.47    and gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
    1.48    and gcd_greatest_int = gcd_greatest [where ?'a = int]
    1.49