src/HOL/Library/FuncSet.thy
changeset 61585 a9599d3d7610
parent 61384 9f5145281888
child 61955 e96292f32c3c
--- a/src/HOL/Library/FuncSet.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/FuncSet.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -226,7 +226,7 @@
 
 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: