# HG changeset patch
# User immler
# Date 1509226357 -7200
# Node ID 4e06b030730c72461b14f909f6bbb079bad726bf
# Parent  149025fecca0562a4d4dda3127fb430c7f459cf8
generalized

diff -r 149025fecca0 -r 4e06b030730c src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Sat Oct 28 21:26:51 2017 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Sat Oct 28 23:32:37 2017 +0200
@@ -210,7 +210,7 @@
 end
 
 
-instance blinfun :: (banach, banach) banach
+instance blinfun :: (real_normed_vector, banach) banach
 proof
   fix X::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   assume "Cauchy X"