Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Bounded_Linear_Function.thy
changeset 81097 6c81cdca5b82
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Oct 02 10:34:41 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Oct 02 10:35:44 2024 +0200
@@ -116,7 +116,7 @@
 
 subsection \<open>Type of bounded linear functions\<close>
 
-typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
+typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>L\<close>\<close>_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
   "{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
   morphisms blinfun_apply Blinfun
   by (blast intro: bounded_linear_intros)
isabelle