changeset 67443 | 3abf6a722518 |
parent 63982 | 4c4049e3bad8 |
child 67457 | 4b921bb461f6 |
--- a/src/HOL/Finite_Set.thy Tue Jan 16 09:12:16 2018 +0100 +++ b/src/HOL/Finite_Set.thy Tue Jan 16 09:30:00 2018 +0100 @@ -67,7 +67,7 @@ subsubsection \<open>Choice principles\<close> -lemma ex_new_if_finite: \<comment> "does not depend on def of finite at all" +lemma ex_new_if_finite: \<comment> \<open>does not depend on def of finite at all\<close> assumes "\<not> finite (UNIV :: 'a set)" and "finite A" shows "\<exists>a::'a. a \<notin> A" proof -