author nipkow Fri Jul 13 15:42:18 2018 +0200 (7 months ago) changeset 68623 b942da0962c2 parent 68622 0987ae51a3be child 68624 205d352ed727 child 68627 e371784becd9
correct import
```     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.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>
```