--- a/src/HOL/List.thy Sun Feb 26 20:08:12 2012 +0100 +++ b/src/HOL/List.thy Mon Feb 27 09:01:49 2012 +0100 @@ -960,6 +960,8 @@ subsubsection {* @{text set} *} +declare set.simps [code_post] --"pretty output" + lemma finite_set [iff]: "finite (set xs)" by (induct xs) auto