IMP/Util distinguishes between sets and functions again; imported only where used.

--- a/src/HOL/IMP/HoareT.thy	Fri Aug 12 20:55:22 2011 -0700
+++ b/src/HOL/IMP/HoareT.thy	Sat Aug 13 11:57:13 2011 +0200
@@ -1,6 +1,6 @@
 header{* Hoare Logic for Total Correctness *}
 
-theory HoareT imports Hoare_Sound_Complete Util begin
+theory HoareT imports Hoare_Sound_Complete begin
 
 text{*
 Now that we have termination, we can define

--- a/src/HOL/IMP/Hoare_Examples.thy	Fri Aug 12 20:55:22 2011 -0700
+++ b/src/HOL/IMP/Hoare_Examples.thy	Sat Aug 13 11:57:13 2011 +0200
@@ -1,6 +1,6 @@
 (* Author: Tobias Nipkow *)
 
-theory Hoare_Examples imports Hoare Util begin
+theory Hoare_Examples imports Hoare begin
 
 subsection{* Example: Sums *}
 

--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Fri Aug 12 20:55:22 2011 -0700
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Sat Aug 13 11:57:13 2011 +0200
@@ -1,4 +1,4 @@
-theory Procs_Dyn_Vars_Dyn imports Util Procs
+theory Procs_Dyn_Vars_Dyn imports Procs
 begin
 
 subsubsection "Dynamic Scoping of Procedures and Variables"

--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Fri Aug 12 20:55:22 2011 -0700
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Sat Aug 13 11:57:13 2011 +0200
@@ -1,4 +1,4 @@
-theory Procs_Stat_Vars_Dyn imports Util Procs
+theory Procs_Stat_Vars_Dyn imports Procs
 begin
 
 subsubsection "Static Scoping of Procedures, Dynamic of Variables"

--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Fri Aug 12 20:55:22 2011 -0700
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Sat Aug 13 11:57:13 2011 +0200
@@ -1,4 +1,4 @@
-theory Procs_Stat_Vars_Stat imports Util Procs
+theory Procs_Stat_Vars_Stat imports Procs
 begin
 
 subsubsection "Static Scoping of Procedures and Variables"

--- a/src/HOL/IMP/Util.thy	Fri Aug 12 20:55:22 2011 -0700
+++ b/src/HOL/IMP/Util.thy	Sat Aug 13 11:57:13 2011 +0200
@@ -5,14 +5,10 @@
 
 subsection "Show sets of variables as lists"
 
-text {* Sets are functions and are not displayed by element if
-computed as values: *}
-value "{''x'', ''y''}"
+text {* Sets may be infinite and are not always displayed by element 
+  if computed as values. Lists do not have this problem. 
 
-text {* Lists do not have this problem *}
-value "[''x'', ''y'']"
-
-text {* We define a function @{text show} that converts a set of
+  We define a function @{text show} that converts a set of
   variable names into a list. To keep things simple, we rely on
   the convention that we only use single letter names.
 *}