changeset 67443 | 3abf6a722518 |
parent 67399 | eab6ce8368fa |
child 67478 | 14d3163588ae |
child 67479 | 31d04ba28893 |
--- a/src/HOL/List.thy Tue Jan 16 09:12:16 2018 +0100 +++ b/src/HOL/List.thy Tue Jan 16 09:30:00 2018 +0100 @@ -1296,7 +1296,7 @@ subsubsection \<open>@{const set}\<close> -declare list.set[code_post] \<comment>"pretty output" +declare list.set[code_post] \<comment> \<open>pretty output\<close> lemma finite_set [iff]: "finite (set xs)" by (induct xs) auto