correct import
authornipkow
Fri Jul 13 15:42:18 2018 +0200 (3 days ago)
changeset 68623b942da0962c2
parent 68622 0987ae51a3be
child 68624 205d352ed727
child 68627 e371784becd9
correct import
src/HOL/Analysis/Inner_Product.thy
src/HOL/Computational_Algebra/Primes.thy
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Fri Jul 13 15:00:38 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Fri Jul 13 15:42:18 2018 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  setup \<open>Sign.add_const_constraint
     1.5    (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
     1.6  
     1.7 -class%important real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
     1.8 +class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
     1.9    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    1.10    assumes inner_commute: "inner x y = inner y x"
    1.11    and inner_add_left: "inner (x + y) z = inner x z + inner y z"
     2.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Fri Jul 13 15:00:38 2018 +0200
     2.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Fri Jul 13 15:42:18 2018 +0200
     2.3 @@ -39,7 +39,7 @@
     2.4  section \<open>Primes\<close>
     2.5  
     2.6  theory Primes
     2.7 -imports HOL.Binomial Euclidean_Algorithm
     2.8 +imports Euclidean_Algorithm
     2.9  begin
    2.10  
    2.11  subsection \<open>Primes on @{typ nat} and @{typ int}\<close>