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: