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