theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
authorwenzelm
Sat Apr 22 22:01:35 2017 +0200 (2017-04-22)
changeset 65552f533820e7248
parent 65551 d164c4fc0d2c
child 65553 006a274cdbc2
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
NEWS
src/Doc/Corec/Corec.thy
src/HOL/Binomial.thy
src/HOL/Codegenerator_Test/Code_Test_GHC.thy
src/HOL/Codegenerator_Test/Code_Test_OCaml.thy
src/HOL/Codegenerator_Test/Code_Test_Scala.thy
src/HOL/Computational_Algebra/Factorial_Ring.thy
src/HOL/GCD.thy
src/HOL/HOLCF/Universal.thy
src/HOL/Import/Import_Setup.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/Stirling.thy
src/HOL/Main.thy
src/HOL/NthRoot.thy
src/HOL/Pre_Main.thy
src/HOL/ROOT
src/HOL/Rat.thy
src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
src/HOL/Transcendental.thy
src/HOL/ex/LocaleTest2.thy
src/HOL/ex/Transfer_Int_Nat.thy
     1.1 --- a/NEWS	Sat Apr 22 12:52:55 2017 +0200
     1.2 +++ b/NEWS	Sat Apr 22 22:01:35 2017 +0200
     1.3 @@ -72,6 +72,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theories "GCD" and "Binomial" are already included in "Main" (instead
     1.8 +of "Complex_Main".
     1.9 +
    1.10  * Constants E/L/F in Library/Formal_Power_Series were renamed to
    1.11  fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space.
    1.12  INCOMPATIBILITY.
     2.1 --- a/src/Doc/Corec/Corec.thy	Sat Apr 22 12:52:55 2017 +0200
     2.2 +++ b/src/Doc/Corec/Corec.thy	Sat Apr 22 22:01:35 2017 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  *)
     2.5  
     2.6  theory Corec
     2.7 -imports GCD "../Datatypes/Setup" "~~/src/HOL/Library/BNF_Corec"
     2.8 +imports Main "../Datatypes/Setup" "~~/src/HOL/Library/BNF_Corec"
     2.9    "~~/src/HOL/Library/FSet"
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/Binomial.thy	Sat Apr 22 12:52:55 2017 +0200
     3.2 +++ b/src/HOL/Binomial.thy	Sat Apr 22 22:01:35 2017 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  section \<open>Combinatorial Functions: Factorial Function, Rising Factorials, Binomial Coefficients and Binomial Theorem\<close>
     3.5  
     3.6  theory Binomial
     3.7 -  imports Main
     3.8 +  imports Pre_Main
     3.9  begin
    3.10  
    3.11  subsection \<open>Factorial\<close>
    3.12 @@ -534,12 +534,12 @@
    3.13  
    3.14  end
    3.15  
    3.16 -lemma pochhammer_nonneg: 
    3.17 +lemma pochhammer_nonneg:
    3.18    fixes x :: "'a :: linordered_semidom"
    3.19    shows "x > 0 \<Longrightarrow> pochhammer x n \<ge> 0"
    3.20    by (induction n) (auto simp: pochhammer_Suc intro!: mult_nonneg_nonneg add_nonneg_nonneg)
    3.21  
    3.22 -lemma pochhammer_pos: 
    3.23 +lemma pochhammer_pos:
    3.24    fixes x :: "'a :: linordered_semidom"
    3.25    shows "x > 0 \<Longrightarrow> pochhammer x n > 0"
    3.26    by (induction n) (auto simp: pochhammer_Suc intro!: mult_pos_pos add_pos_nonneg)
    3.27 @@ -1616,7 +1616,7 @@
    3.28    qed
    3.29  qed
    3.30  
    3.31 -lemma card_disjoint_shuffle: 
    3.32 +lemma card_disjoint_shuffle:
    3.33    assumes "set xs \<inter> set ys = {}"
    3.34    shows   "card (shuffle xs ys) = (length xs + length ys) choose length xs"
    3.35  using assms
    3.36 @@ -1634,7 +1634,7 @@
    3.37      by (rule card_image) auto
    3.38    also have "\<dots> = (length (x # xs) + length ys) choose length (x # xs)"
    3.39      using "3.prems" by (intro "3.IH") auto
    3.40 -  also have "length xs + length (y # ys) choose length xs + \<dots> = 
    3.41 +  also have "length xs + length (y # ys) choose length xs + \<dots> =
    3.42                 (length (x # xs) + length (y # ys)) choose length (x # xs)" by simp
    3.43    finally show ?case .
    3.44  qed auto
     4.1 --- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sat Apr 22 12:52:55 2017 +0200
     4.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sat Apr 22 22:01:35 2017 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  Test case for test_code on GHC
     4.5  *)
     4.6  
     4.7 -theory Code_Test_GHC imports "../Library/Code_Test" "../GCD" begin
     4.8 +theory Code_Test_GHC imports "../Library/Code_Test" begin
     4.9  
    4.10  test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
    4.11  
     5.1 --- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Sat Apr 22 12:52:55 2017 +0200
     5.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Sat Apr 22 22:01:35 2017 +0200
     5.3 @@ -4,7 +4,7 @@
     5.4  Test case for test_code on OCaml
     5.5  *)
     5.6  
     5.7 -theory Code_Test_OCaml imports  "../Library/Code_Test" "../GCD" begin
     5.8 +theory Code_Test_OCaml imports  "../Library/Code_Test" begin
     5.9  
    5.10  test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
    5.11  
     6.1 --- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Sat Apr 22 12:52:55 2017 +0200
     6.2 +++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Sat Apr 22 22:01:35 2017 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4  Test case for test_code on Scala
     6.5  *)
     6.6  
     6.7 -theory Code_Test_Scala imports  "../Library/Code_Test" "../GCD" begin 
     6.8 +theory Code_Test_Scala imports  "../Library/Code_Test" begin
     6.9  
    6.10  declare [[scala_case_insensitive]]
    6.11  
     7.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Apr 22 12:52:55 2017 +0200
     7.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Apr 22 22:01:35 2017 +0200
     7.3 @@ -6,9 +6,8 @@
     7.4  section \<open>Factorial (semi)rings\<close>
     7.5  
     7.6  theory Factorial_Ring
     7.7 -imports 
     7.8 +imports
     7.9    Main
    7.10 -  "../GCD"
    7.11    "~~/src/HOL/Library/Multiset"
    7.12  begin
    7.13  
    7.14 @@ -66,7 +65,7 @@
    7.15    shows "p \<noteq> 0"
    7.16    using assms by (auto intro: ccontr)
    7.17  
    7.18 -lemma prime_elem_dvd_power: 
    7.19 +lemma prime_elem_dvd_power:
    7.20    "prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
    7.21    by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
    7.22  
    7.23 @@ -111,7 +110,7 @@
    7.24    with \<open>irreducible p\<close> show False
    7.25      by (simp add: irreducible_not_unit)
    7.26  qed
    7.27 -   
    7.28 +
    7.29  lemma unit_imp_no_prime_divisors:
    7.30    assumes "is_unit x" "prime_elem p"
    7.31    shows   "\<not>p dvd x"
    7.32 @@ -261,13 +260,13 @@
    7.33      using p prime_elem_dvd_mult_iff by blast
    7.34    then show ?thesis
    7.35    proof cases
    7.36 -    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
    7.37 +    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel)
    7.38        then have "\<exists>x. k dvd x * n \<and> m = p * x"
    7.39          using p pk by (auto simp: mult.assoc)
    7.40      then show ?thesis ..
    7.41    next
    7.42 -    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) 
    7.43 -    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" 
    7.44 +    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel)
    7.45 +    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y"
    7.46        by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
    7.47      then show ?thesis ..
    7.48    qed
    7.49 @@ -285,13 +284,13 @@
    7.50      using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
    7.51    then show ?case
    7.52    proof cases
    7.53 -    case (1 x) 
    7.54 +    case (1 x)
    7.55      with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast
    7.56      with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
    7.57        by (auto intro: mult_dvd_mono)
    7.58      thus ?thesis by blast
    7.59    next
    7.60 -    case (2 y) 
    7.61 +    case (2 y)
    7.62      with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast
    7.63      with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
    7.64        by (auto intro: mult_dvd_mono)
    7.65 @@ -325,7 +324,7 @@
    7.66    assumes "prime_elem p"
    7.67    assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
    7.68    shows "p ^ n dvd b"
    7.69 -  using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> 
    7.70 +  using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close>
    7.71  proof (induct n arbitrary: b)
    7.72    case 0 then show ?case by simp
    7.73  next
    7.74 @@ -454,7 +453,7 @@
    7.75  lemma prime_dvd_mult_iff: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
    7.76    by (auto dest: prime_dvd_multD)
    7.77  
    7.78 -lemma prime_dvd_power: 
    7.79 +lemma prime_dvd_power:
    7.80    "prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
    7.81    by (auto dest!: prime_elem_dvd_power simp: prime_def)
    7.82  
    7.83 @@ -610,11 +609,11 @@
    7.84    shows   "coprime p n"
    7.85    using assms by (simp add: prime_elem_imp_coprime)
    7.86  
    7.87 -lemma prime_elem_imp_power_coprime: 
    7.88 +lemma prime_elem_imp_power_coprime:
    7.89    "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
    7.90    by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
    7.91  
    7.92 -lemma prime_imp_power_coprime: 
    7.93 +lemma prime_imp_power_coprime:
    7.94    "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
    7.95    by (simp add: prime_elem_imp_power_coprime)
    7.96  
    7.97 @@ -625,12 +624,12 @@
    7.98  proof -
    7.99    from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
   7.100      by (auto simp: coprime prime_elem_def)
   7.101 -  with p have "coprime (p^n) a \<or> coprime (p^n) b" 
   7.102 +  with p have "coprime (p^n) a \<or> coprime (p^n) b"
   7.103      by (auto intro: prime_elem_imp_coprime coprime_exp_left)
   7.104    with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
   7.105  qed
   7.106  
   7.107 -lemma primes_coprime: 
   7.108 +lemma primes_coprime:
   7.109    "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   7.110    using prime_imp_coprime primes_dvd_imp_eq by blast
   7.111  
   7.112 @@ -644,7 +643,7 @@
   7.113      "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
   7.114  
   7.115  text \<open>Alternative characterization\<close>
   7.116 -  
   7.117 +
   7.118  lemma (in normalization_semidom) factorial_semiring_altI_aux:
   7.119    assumes finite_divisors: "\<And>x. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
   7.120    assumes irreducible_imp_prime_elem: "\<And>x. irreducible x \<Longrightarrow> prime_elem x"
   7.121 @@ -703,14 +702,14 @@
   7.122        from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
   7.123      qed
   7.124    qed
   7.125 -qed 
   7.126 +qed
   7.127  
   7.128  lemma factorial_semiring_altI:
   7.129    assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
   7.130    assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
   7.131    shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
   7.132    by intro_classes (rule factorial_semiring_altI_aux[OF assms])
   7.133 -  
   7.134 +
   7.135  text \<open>Properties\<close>
   7.136  
   7.137  context factorial_semiring
   7.138 @@ -912,7 +911,7 @@
   7.139  lemma prime_multiplicity_other:
   7.140    assumes "prime p" "prime q" "p \<noteq> q"
   7.141    shows   "multiplicity p q = 0"
   7.142 -  using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)  
   7.143 +  using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)
   7.144  
   7.145  lemma prime_multiplicity_gt_zero_iff:
   7.146    "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   7.147 @@ -1057,7 +1056,7 @@
   7.148    also have "multiplicity p \<dots> = multiplicity p x"
   7.149      by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
   7.150    finally show ?thesis .
   7.151 -qed simp_all   
   7.152 +qed simp_all
   7.153  
   7.154  lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
   7.155    by (rule multiplicity_self) auto
   7.156 @@ -1272,13 +1271,13 @@
   7.157  proof -
   7.158    have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
   7.159      by (subst count_prime_factorization_prime) (simp_all add: assms)
   7.160 -  also from assms 
   7.161 +  also from assms
   7.162      have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
   7.163        by (intro prime_factorization_mult)
   7.164 -  also have "count \<dots> (normalize p) = 
   7.165 +  also have "count \<dots> (normalize p) =
   7.166      count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
   7.167      by simp
   7.168 -  also have "\<dots> = multiplicity p x + multiplicity p y" 
   7.169 +  also have "\<dots> = multiplicity p x + multiplicity p y"
   7.170      by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
   7.171    finally show ?thesis .
   7.172  qed
   7.173 @@ -1300,7 +1299,7 @@
   7.174  proof -
   7.175    have "multiplicity p (prod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
   7.176      using assms by (subst prod_unfold_prod_mset)
   7.177 -                   (simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset 
   7.178 +                   (simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset
   7.179                        multiset.map_comp o_def)
   7.180    also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
   7.181      by (induction A rule: finite_induct) simp_all
   7.182 @@ -1330,7 +1329,7 @@
   7.183    finally show ?thesis ..
   7.184  qed
   7.185  
   7.186 -lemma prime_factorization_subset_imp_dvd: 
   7.187 +lemma prime_factorization_subset_imp_dvd:
   7.188    "x \<noteq> 0 \<Longrightarrow> (prime_factorization x \<subseteq># prime_factorization y) \<Longrightarrow> x dvd y"
   7.189    by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd)
   7.190  
   7.191 @@ -1361,7 +1360,7 @@
   7.192    also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
   7.193      by (subst prod_mset_multiplicity) simp_all
   7.194    also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
   7.195 -    by (intro prod.cong) 
   7.196 +    by (intro prod.cong)
   7.197        (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
   7.198    finally show ?thesis ..
   7.199  qed
   7.200 @@ -1381,23 +1380,23 @@
   7.201      by (simp only: set_mset_def)
   7.202    from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
   7.203    also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A)
   7.204 -  also from nz have "normalize n = prod_mset (prime_factorization n)" 
   7.205 +  also from nz have "normalize n = prod_mset (prime_factorization n)"
   7.206      by (simp add: prod_mset_prime_factorization)
   7.207 -  finally have "prime_factorization (prod_mset A) = 
   7.208 +  finally have "prime_factorization (prod_mset A) =
   7.209                    prime_factorization (prod_mset (prime_factorization n))" by simp
   7.210    also from S(1) have "prime_factorization (prod_mset A) = A"
   7.211      by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
   7.212    also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
   7.213      by (intro prime_factorization_prod_mset_primes) auto
   7.214    finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric])
   7.215 -  
   7.216 +
   7.217    show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
   7.218    proof safe
   7.219      fix p :: 'a assume p: "prime p"
   7.220      have "multiplicity p n = multiplicity p (normalize n)" by simp
   7.221 -    also have "normalize n = prod_mset A" 
   7.222 +    also have "normalize n = prod_mset A"
   7.223        by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S)
   7.224 -    also from p set_mset_A S(1) 
   7.225 +    also from p set_mset_A S(1)
   7.226      have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
   7.227        by (intro prime_elem_multiplicity_prod_mset_distrib) auto
   7.228      also from S(1) p
   7.229 @@ -1408,7 +1407,7 @@
   7.230    qed
   7.231  qed
   7.232  
   7.233 -lemma prime_factors_product: 
   7.234 +lemma prime_factors_product:
   7.235    "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
   7.236    by (simp add: prime_factorization_mult)
   7.237  
   7.238 @@ -1454,7 +1453,7 @@
   7.239    "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b"
   7.240    by (simp add: multiplicity_def)
   7.241  
   7.242 -lemma not_dvd_imp_multiplicity_0: 
   7.243 +lemma not_dvd_imp_multiplicity_0:
   7.244    assumes "\<not>p dvd x"
   7.245    shows   "multiplicity p x = 0"
   7.246  proof -
   7.247 @@ -1740,11 +1739,11 @@
   7.248  
   7.249  lemma
   7.250    assumes "x \<noteq> 0" "y \<noteq> 0"
   7.251 -  shows gcd_eq_factorial': 
   7.252 -          "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y. 
   7.253 +  shows gcd_eq_factorial':
   7.254 +          "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y.
   7.255                            p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
   7.256      and lcm_eq_factorial':
   7.257 -          "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y. 
   7.258 +          "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y.
   7.259                            p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2")
   7.260  proof -
   7.261    have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
   7.262 @@ -1784,7 +1783,7 @@
   7.263    case False
   7.264    hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))"
   7.265      by (intro associatedI prime_factorization_subset_imp_dvd)
   7.266 -       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
   7.267 +       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm
   7.268            subset_mset.inf_sup_distrib1)
   7.269    thus ?thesis by simp
   7.270  qed
   7.271 @@ -1799,7 +1798,7 @@
   7.272    case False
   7.273    hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))"
   7.274      by (intro associatedI prime_factorization_subset_imp_dvd)
   7.275 -       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
   7.276 +       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm
   7.277            subset_mset.sup_inf_distrib1)
   7.278    thus ?thesis by simp
   7.279  qed
     8.1 --- a/src/HOL/GCD.thy	Sat Apr 22 12:52:55 2017 +0200
     8.2 +++ b/src/HOL/GCD.thy	Sat Apr 22 22:01:35 2017 +0200
     8.3 @@ -31,12 +31,12 @@
     8.4  section \<open>Greatest common divisor and least common multiple\<close>
     8.5  
     8.6  theory GCD
     8.7 -  imports Main
     8.8 +  imports Pre_Main
     8.9  begin
    8.10  
    8.11  subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
    8.12 -  
    8.13 -locale bounded_quasi_semilattice = abel_semigroup + 
    8.14 +
    8.15 +locale bounded_quasi_semilattice = abel_semigroup +
    8.16    fixes top :: 'a  ("\<top>") and bot :: 'a  ("\<bottom>")
    8.17      and normalize :: "'a \<Rightarrow> 'a"
    8.18    assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
    8.19 @@ -65,7 +65,7 @@
    8.20  lemma top_right_normalize [simp]:
    8.21    "a \<^bold>* \<top> = normalize a"
    8.22    using top_left_normalize [of a] by (simp add: ac_simps)
    8.23 -  
    8.24 +
    8.25  lemma bottom_right_bottom [simp]:
    8.26    "a \<^bold>* \<bottom> = \<bottom>"
    8.27    using bottom_left_bottom [of a] by (simp add: ac_simps)
    8.28 @@ -74,7 +74,7 @@
    8.29    "a \<^bold>* normalize b = a \<^bold>* b"
    8.30    using normalize_left_idem [of b a] by (simp add: ac_simps)
    8.31  
    8.32 -end    
    8.33 +end
    8.34  
    8.35  locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
    8.36  begin
    8.37 @@ -134,7 +134,7 @@
    8.38    assumes "B \<subseteq> A"
    8.39    shows "F B \<^bold>* F A = F A"
    8.40    using assms by (simp add: union [symmetric] Un_absorb1)
    8.41 -  
    8.42 +
    8.43  end
    8.44  
    8.45  subsection \<open>Abstract GCD and LCM\<close>
    8.46 @@ -282,7 +282,7 @@
    8.47    show "coprime 1 a" for a
    8.48      by (rule associated_eqI) simp_all
    8.49  qed simp_all
    8.50 -  
    8.51 +
    8.52  lemma gcd_self: "gcd a a = normalize a"
    8.53    by (fact gcd.idem_normalize)
    8.54  
    8.55 @@ -1071,7 +1071,7 @@
    8.56    moreover from assms have "p dvd gcd (b * a) (b * p)"
    8.57      by (intro gcd_greatest) (simp_all add: mult.commute)
    8.58    hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
    8.59 -  with False have "y dvd b" 
    8.60 +  with False have "y dvd b"
    8.61      by (simp add: x_def y_def div_dvd_iff_mult assms)
    8.62    ultimately show ?thesis by (rule that)
    8.63  qed
    8.64 @@ -1527,7 +1527,7 @@
    8.65  
    8.66  end
    8.67  
    8.68 -  
    8.69 +
    8.70  subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
    8.71  
    8.72  context semiring_gcd
    8.73 @@ -1546,15 +1546,15 @@
    8.74  
    8.75  abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
    8.76    where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
    8.77 -    
    8.78 +
    8.79  lemma Gcd_fin_dvd:
    8.80    "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
    8.81 -  by (induct A rule: infinite_finite_induct) 
    8.82 +  by (induct A rule: infinite_finite_induct)
    8.83      (auto intro: dvd_trans)
    8.84  
    8.85  lemma dvd_Lcm_fin:
    8.86    "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
    8.87 -  by (induct A rule: infinite_finite_induct) 
    8.88 +  by (induct A rule: infinite_finite_induct)
    8.89      (auto intro: dvd_trans)
    8.90  
    8.91  lemma Gcd_fin_greatest:
    8.92 @@ -1580,7 +1580,7 @@
    8.93  lemma dvd_gcd_list_iff:
    8.94    "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"
    8.95    by (simp add: dvd_Gcd_fin_iff)
    8.96 -  
    8.97 +
    8.98  lemma Lcm_fin_dvd_iff:
    8.99    "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b  \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
   8.100    using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])
     9.1 --- a/src/HOL/HOLCF/Universal.thy	Sat Apr 22 12:52:55 2017 +0200
     9.2 +++ b/src/HOL/HOLCF/Universal.thy	Sat Apr 22 22:01:35 2017 +0200
     9.3 @@ -8,6 +8,8 @@
     9.4  imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
     9.5  begin
     9.6  
     9.7 +no_notation binomial  (infixl "choose" 65)
     9.8 +
     9.9  subsection \<open>Basis for universal domain\<close>
    9.10  
    9.11  subsubsection \<open>Basis datatype\<close>
    9.12 @@ -976,7 +978,7 @@
    9.13  apply (simp add: udom_approx_principal)
    9.14  apply (simp add: ubasis_until_same ubasis_le_refl)
    9.15  done
    9.16 - 
    9.17 +
    9.18  lemma udom_approx [simp]: "approx_chain udom_approx"
    9.19  proof
    9.20    show "chain (\<lambda>i. udom_approx i)"
    9.21 @@ -990,4 +992,6 @@
    9.22  
    9.23  hide_const (open) node
    9.24  
    9.25 +notation binomial  (infixl "choose" 65)
    9.26 +
    9.27  end
    10.1 --- a/src/HOL/Import/Import_Setup.thy	Sat Apr 22 12:52:55 2017 +0200
    10.2 +++ b/src/HOL/Import/Import_Setup.thy	Sat Apr 22 22:01:35 2017 +0200
    10.3 @@ -6,7 +6,7 @@
    10.4  section \<open>Importer machinery and required theorems\<close>
    10.5  
    10.6  theory Import_Setup
    10.7 -imports Main "~~/src/HOL/Binomial"
    10.8 +imports Main
    10.9  keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
   10.10  begin
   10.11  
    11.1 --- a/src/HOL/Library/Code_Target_Int.thy	Sat Apr 22 12:52:55 2017 +0200
    11.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Sat Apr 22 22:01:35 2017 +0200
    11.3 @@ -5,7 +5,7 @@
    11.4  section \<open>Implementation of integer numbers by target-language integers\<close>
    11.5  
    11.6  theory Code_Target_Int
    11.7 -imports "../GCD"
    11.8 +imports Main
    11.9  begin
   11.10  
   11.11  code_datatype int_of_integer
   11.12 @@ -22,11 +22,11 @@
   11.13  
   11.14  lemma [code]:
   11.15    "Int.Pos = int_of_integer \<circ> integer_of_num"
   11.16 -  by transfer (simp add: fun_eq_iff) 
   11.17 +  by transfer (simp add: fun_eq_iff)
   11.18  
   11.19  lemma [code]:
   11.20    "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
   11.21 -  by transfer (simp add: fun_eq_iff) 
   11.22 +  by transfer (simp add: fun_eq_iff)
   11.23  
   11.24  lemma [code_abbrev]:
   11.25    "int_of_integer (numeral k) = Int.Pos k"
   11.26 @@ -37,7 +37,7 @@
   11.27    by transfer simp
   11.28  
   11.29  context
   11.30 -begin  
   11.31 +begin
   11.32  
   11.33  qualified definition positive :: "num \<Rightarrow> int"
   11.34    where [simp]: "positive = numeral"
    12.1 --- a/src/HOL/Library/Permutations.thy	Sat Apr 22 12:52:55 2017 +0200
    12.2 +++ b/src/HOL/Library/Permutations.thy	Sat Apr 22 22:01:35 2017 +0200
    12.3 @@ -5,7 +5,7 @@
    12.4  section \<open>Permutations, both general and specifically on finite sets.\<close>
    12.5  
    12.6  theory Permutations
    12.7 -  imports Binomial Multiset Disjoint_Sets
    12.8 +  imports Multiset Disjoint_Sets
    12.9  begin
   12.10  
   12.11  subsection \<open>Transpositions\<close>
    13.1 --- a/src/HOL/Library/Stirling.thy	Sat Apr 22 12:52:55 2017 +0200
    13.2 +++ b/src/HOL/Library/Stirling.thy	Sat Apr 22 22:01:35 2017 +0200
    13.3 @@ -8,7 +8,7 @@
    13.4  section \<open>Stirling numbers of first and second kind\<close>
    13.5  
    13.6  theory Stirling
    13.7 -imports Binomial
    13.8 +imports Main
    13.9  begin
   13.10  
   13.11  subsection \<open>Stirling numbers of the second kind\<close>
    14.1 --- a/src/HOL/Main.thy	Sat Apr 22 12:52:55 2017 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,42 +0,0 @@
    14.4 -section \<open>Main HOL\<close>
    14.5 -
    14.6 -theory Main
    14.7 -imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
    14.8 -begin
    14.9 -
   14.10 -text \<open>
   14.11 -  Classical Higher-order Logic -- only ``Main'', excluding real and
   14.12 -  complex numbers etc.
   14.13 -\<close>
   14.14 -
   14.15 -no_notation
   14.16 -  bot ("\<bottom>") and
   14.17 -  top ("\<top>") and
   14.18 -  inf (infixl "\<sqinter>" 70) and
   14.19 -  sup (infixl "\<squnion>" 65) and
   14.20 -  Inf ("\<Sqinter>_" [900] 900) and
   14.21 -  Sup ("\<Squnion>_" [900] 900) and
   14.22 -  ordLeq2 (infix "<=o" 50) and
   14.23 -  ordLeq3 (infix "\<le>o" 50) and
   14.24 -  ordLess2 (infix "<o" 50) and
   14.25 -  ordIso2 (infix "=o" 50) and
   14.26 -  card_of ("|_|") and
   14.27 -  csum (infixr "+c" 65) and
   14.28 -  cprod (infixr "*c" 80) and
   14.29 -  cexp (infixr "^c" 90) and
   14.30 -  convol ("\<langle>(_,/ _)\<rangle>")
   14.31 -
   14.32 -hide_const (open)
   14.33 -  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
   14.34 -  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
   14.35 -  shift proj id_bnf
   14.36 -
   14.37 -hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
   14.38 -
   14.39 -no_syntax
   14.40 -  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   14.41 -  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   14.42 -  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   14.43 -  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   14.44 -
   14.45 -end
    15.1 --- a/src/HOL/NthRoot.thy	Sat Apr 22 12:52:55 2017 +0200
    15.2 +++ b/src/HOL/NthRoot.thy	Sat Apr 22 22:01:35 2017 +0200
    15.3 @@ -6,7 +6,7 @@
    15.4  section \<open>Nth Roots of Real Numbers\<close>
    15.5  
    15.6  theory NthRoot
    15.7 -  imports Deriv Binomial
    15.8 +  imports Deriv
    15.9  begin
   15.10  
   15.11  
   15.12 @@ -469,7 +469,7 @@
   15.13  lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
   15.14    using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
   15.15  
   15.16 -lemma real_sqrt_power_even: 
   15.17 +lemma real_sqrt_power_even:
   15.18    assumes "even n" "x \<ge> 0"
   15.19    shows   "sqrt x ^ n = x ^ (n div 2)"
   15.20  proof -
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Pre_Main.thy	Sat Apr 22 22:01:35 2017 +0200
    16.3 @@ -0,0 +1,42 @@
    16.4 +section \<open>Main HOL\<close>
    16.5 +
    16.6 +theory Pre_Main
    16.7 +imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
    16.8 +begin
    16.9 +
   16.10 +text \<open>
   16.11 +  Classical Higher-order Logic -- only ``Main'', excluding real and
   16.12 +  complex numbers etc.
   16.13 +\<close>
   16.14 +
   16.15 +no_notation
   16.16 +  bot ("\<bottom>") and
   16.17 +  top ("\<top>") and
   16.18 +  inf (infixl "\<sqinter>" 70) and
   16.19 +  sup (infixl "\<squnion>" 65) and
   16.20 +  Inf ("\<Sqinter>_" [900] 900) and
   16.21 +  Sup ("\<Squnion>_" [900] 900) and
   16.22 +  ordLeq2 (infix "<=o" 50) and
   16.23 +  ordLeq3 (infix "\<le>o" 50) and
   16.24 +  ordLess2 (infix "<o" 50) and
   16.25 +  ordIso2 (infix "=o" 50) and
   16.26 +  card_of ("|_|") and
   16.27 +  csum (infixr "+c" 65) and
   16.28 +  cprod (infixr "*c" 80) and
   16.29 +  cexp (infixr "^c" 90) and
   16.30 +  convol ("\<langle>(_,/ _)\<rangle>")
   16.31 +
   16.32 +hide_const (open)
   16.33 +  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
   16.34 +  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
   16.35 +  shift proj id_bnf
   16.36 +
   16.37 +hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
   16.38 +
   16.39 +no_syntax
   16.40 +  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   16.41 +  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   16.42 +  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   16.43 +  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
   16.44 +
   16.45 +end
    17.1 --- a/src/HOL/ROOT	Sat Apr 22 12:52:55 2017 +0200
    17.2 +++ b/src/HOL/ROOT	Sat Apr 22 22:01:35 2017 +0200
    17.3 @@ -23,8 +23,6 @@
    17.4    sessions
    17.5      "HOL-Library"
    17.6    theories
    17.7 -    GCD
    17.8 -    Binomial
    17.9      "HOL-Library.Old_Datatype"
   17.10    files
   17.11      "Tools/Quickcheck/Narrowing_Engine.hs"
    18.1 --- a/src/HOL/Rat.thy	Sat Apr 22 12:52:55 2017 +0200
    18.2 +++ b/src/HOL/Rat.thy	Sat Apr 22 22:01:35 2017 +0200
    18.3 @@ -5,7 +5,7 @@
    18.4  section \<open>Rational numbers\<close>
    18.5  
    18.6  theory Rat
    18.7 -  imports GCD Archimedean_Field
    18.8 +  imports Archimedean_Field
    18.9  begin
   18.10  
   18.11  subsection \<open>Rational numbers as quotient\<close>
   18.12 @@ -403,7 +403,7 @@
   18.13  
   18.14  lemma quotient_of_denom_pos': "snd (quotient_of r) > 0"
   18.15    using quotient_of_denom_pos [of r] by (simp add: prod_eq_iff)
   18.16 -    
   18.17 +
   18.18  lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q"
   18.19    by (cases r) (simp add: quotient_of_Fract normalize_coprime)
   18.20  
    19.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sat Apr 22 12:52:55 2017 +0200
    19.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sat Apr 22 22:01:35 2017 +0200
    19.3 @@ -4,7 +4,7 @@
    19.4  *)
    19.5  
    19.6  theory Greatest_Common_Divisor
    19.7 -imports "../../SPARK" GCD
    19.8 +imports "../../SPARK"
    19.9  begin
   19.10  
   19.11  spark_proof_functions
    20.1 --- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Sat Apr 22 12:52:55 2017 +0200
    20.2 +++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Sat Apr 22 22:01:35 2017 +0200
    20.3 @@ -4,7 +4,7 @@
    20.4  *)
    20.5  
    20.6  theory Simple_Greatest_Common_Divisor
    20.7 -imports "../SPARK" GCD
    20.8 +imports "../SPARK"
    20.9  begin
   20.10  
   20.11  spark_proof_functions
    21.1 --- a/src/HOL/Transcendental.thy	Sat Apr 22 12:52:55 2017 +0200
    21.2 +++ b/src/HOL/Transcendental.thy	Sat Apr 22 22:01:35 2017 +0200
    21.3 @@ -7,7 +7,7 @@
    21.4  section \<open>Power Series, Transcendental Functions etc.\<close>
    21.5  
    21.6  theory Transcendental
    21.7 -imports Binomial Series Deriv NthRoot
    21.8 +imports Series Deriv NthRoot
    21.9  begin
   21.10  
   21.11  text \<open>A fact theorem on reals.\<close>
   21.12 @@ -74,7 +74,7 @@
   21.13  subsection \<open>More facts about binomial coefficients\<close>
   21.14  
   21.15  text \<open>
   21.16 -  These facts could have been proven before, but having real numbers 
   21.17 +  These facts could have been proven before, but having real numbers
   21.18    makes the proofs a lot easier.
   21.19  \<close>
   21.20  
   21.21 @@ -115,11 +115,11 @@
   21.22    thus ?thesis
   21.23    proof (induction rule: inc_induct)
   21.24      case base
   21.25 -    with assms binomial_less_binomial_Suc[of "k' - 1" n] 
   21.26 +    with assms binomial_less_binomial_Suc[of "k' - 1" n]
   21.27        show ?case by simp
   21.28    next
   21.29      case (step k)
   21.30 -    from step.prems step.hyps assms have "n choose k < n choose (Suc k)" 
   21.31 +    from step.prems step.hyps assms have "n choose k < n choose (Suc k)"
   21.32        by (intro binomial_less_binomial_Suc) simp_all
   21.33      also have "\<dots> < n choose k'" by (rule step.IH)
   21.34      finally show ?case .
   21.35 @@ -150,12 +150,12 @@
   21.36    proof (cases "k = n div 2 \<and> odd n")
   21.37      case False
   21.38      with assms(2) have "2*k \<ge> n" by presburger
   21.39 -    with not_eq assms binomial_strict_antimono[of k k' n] 
   21.40 +    with not_eq assms binomial_strict_antimono[of k k' n]
   21.41        show ?thesis by simp
   21.42    next
   21.43      case True
   21.44      have "n choose k' \<le> n choose (Suc (n div 2))"
   21.45 -    proof (cases "k' = Suc (n div 2)") 
   21.46 +    proof (cases "k' = Suc (n div 2)")
   21.47        case False
   21.48        with assms True not_eq have "Suc (n div 2) < k'" by simp
   21.49        with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True
   21.50 @@ -191,10 +191,10 @@
   21.51      have "4 ^ n = (\<Sum>k=0..2*n. (2*n) choose k)"
   21.52      by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def)
   21.53    also have "{0..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto
   21.54 -  also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) = 
   21.55 +  also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) =
   21.56                 (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
   21.57      by (subst sum.union_disjoint) auto
   21.58 -  also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)" 
   21.59 +  also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)"
   21.60      by (cases n) simp_all
   21.61    also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)"
   21.62      by (intro sum_mono3) auto
   21.63 @@ -959,7 +959,7 @@
   21.64    have summable: "summable (\<lambda>n. diffs c n * z^n)"
   21.65      by (intro termdiff_converges[OF norm] sums_summable[OF sums])
   21.66    from norm have "eventually (\<lambda>z. z \<in> norm -` {..<K}) (nhds z)"
   21.67 -    by (intro eventually_nhds_in_open open_vimage) 
   21.68 +    by (intro eventually_nhds_in_open open_vimage)
   21.69         (simp_all add: continuous_on_norm continuous_on_id)
   21.70    hence eq: "eventually (\<lambda>z. (\<Sum>n. c n * z^n) = f z) (nhds z)"
   21.71      by eventually_elim (insert sums, simp add: sums_iff)
    22.1 --- a/src/HOL/ex/LocaleTest2.thy	Sat Apr 22 12:52:55 2017 +0200
    22.2 +++ b/src/HOL/ex/LocaleTest2.thy	Sat Apr 22 22:01:35 2017 +0200
    22.3 @@ -11,7 +11,7 @@
    22.4  section \<open>Test of Locale Interpretation\<close>
    22.5  
    22.6  theory LocaleTest2
    22.7 -imports Main GCD
    22.8 +imports Main
    22.9  begin
   22.10  
   22.11  section \<open>Interpretation of Defined Concepts\<close>
    23.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Sat Apr 22 12:52:55 2017 +0200
    23.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Sat Apr 22 22:01:35 2017 +0200
    23.3 @@ -5,7 +5,7 @@
    23.4  section \<open>Using the transfer method between nat and int\<close>
    23.5  
    23.6  theory Transfer_Int_Nat
    23.7 -imports GCD
    23.8 +imports Main
    23.9  begin
   23.10  
   23.11  subsection \<open>Correspondence relation\<close>
   23.12 @@ -15,7 +15,7 @@
   23.13  
   23.14  subsection \<open>Transfer domain rules\<close>
   23.15  
   23.16 -lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)" 
   23.17 +lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)"
   23.18    unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int)
   23.19  
   23.20  subsection \<open>Transfer rules\<close>
   23.21 @@ -177,7 +177,7 @@
   23.22  done
   23.23  
   23.24  lemma
   23.25 -  assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> 
   23.26 +  assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow>
   23.27      sum_list [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
   23.28    shows "sum_list [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
   23.29  apply transfer