src/HOL/Library/FuncSet.thy
changeset 61585 a9599d3d7610
parent 61384 9f5145281888
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Library/FuncSet.thy	Thu Nov 05 10:35:37 2015 +0100
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Thu Nov 05 10:39:49 2015 +0100
     1.3 @@ -226,7 +226,7 @@
     1.4  
     1.5  subsection \<open>Bijections Between Sets\<close>
     1.6  
     1.7 -text \<open>The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
     1.8 +text \<open>The definition of @{const bij_betw} is in \<open>Fun.thy\<close>, but most of
     1.9  the theorems belong here, or need at least @{term Hilbert_Choice}.\<close>
    1.10  
    1.11  lemma bij_betwI: