src/HOL/Library/FuncSet.thy

   by (auto simp: restrict_def Pi_def)
 
 
 subsection \<open>Bijections Between Sets\<close>
 
-text \<open>The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
+text \<open>The definition of @{const bij_betw} is in \<open>Fun.thy\<close>, but most of
 the theorems belong here, or need at least @{term Hilbert_Choice}.\<close>
 
 lemma bij_betwI:
   assumes "f \<in> A \<rightarrow> B"
     and "g \<in> B \<rightarrow> A"