--- 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"
--- 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>