Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generalized
authorimmler
Sat, 28 Oct 2017 23:32:37 +0200
changeset 66933 4e06b030730c
parent 66932 149025fecca0
child 66934 b86513bcf7ac
generalized
src/HOL/Analysis/Bounded_Linear_Function.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle