generalized
authorimmler
Sat Oct 28 23:32:37 2017 +0200 (19 months ago)
changeset 669334e06b030730c
parent 66932 149025fecca0
child 66934 b86513bcf7ac
generalized
src/HOL/Analysis/Bounded_Linear_Function.thy
     1.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Sat Oct 28 21:26:51 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Sat Oct 28 23:32:37 2017 +0200
     1.3 @@ -210,7 +210,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -instance blinfun :: (banach, banach) banach
     1.8 +instance blinfun :: (real_normed_vector, banach) banach
     1.9  proof
    1.10    fix X::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
    1.11    assume "Cauchy X"