# HG changeset patch
# User nipkow
# Date 1330329709 -3600
# Node ID f1dfcf8be88d7e3980e00e651f805264fe8be3bd
# Parent  07f9732804ad26d87b98b2b2b58788ab6291e4d2
converting "set [...]" to "{...}" in evaluation results

diff -r 07f9732804ad -r f1dfcf8be88d src/HOL/List.thy
--- 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