converting "set [...]" to "{...}" in evaluation results
authornipkow
Mon Feb 27 09:01:49 2012 +0100 (2012-02-27)
changeset 46698f1dfcf8be88d
parent 46690 07f9732804ad
child 46699 ae3f30a5063a
converting "set [...]" to "{...}" in evaluation results
src/HOL/List.thy
     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