# HG changeset patch
# User nipkow
# Date 1531489338 -7200
# Node ID b942da0962c25b78202fa13ff5a255dc9393cd02
# Parent  0987ae51a3be79d21caa2257546eb9cad912e473
correct import

diff -r 0987ae51a3be -r b942da0962c2 src/HOL/Analysis/Inner_Product.thy
--- a/src/HOL/Analysis/Inner_Product.thy	Fri Jul 13 15:00:38 2018 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy	Fri Jul 13 15:42:18 2018 +0200
@@ -27,7 +27,7 @@
 setup \<open>Sign.add_const_constraint
   (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
 
-class%important real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
+class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
   and inner_add_left: "inner (x + y) z = inner x z + inner y z"
diff -r 0987ae51a3be -r b942da0962c2 src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Fri Jul 13 15:00:38 2018 +0200
+++ b/src/HOL/Computational_Algebra/Primes.thy	Fri Jul 13 15:42:18 2018 +0200
@@ -39,7 +39,7 @@
 section \<open>Primes\<close>
 
 theory Primes
-imports HOL.Binomial Euclidean_Algorithm
+imports Euclidean_Algorithm
 begin
 
 subsection \<open>Primes on @{typ nat} and @{typ int}\<close>