# HG changeset patch
# User kleing
# Date 1313229433 -7200
# Node ID b4b5cbca25193f02a9e86ee88a1698c92a972b5e
# Parent  eda112e9cdeee98a1a6f6023e301a2c5ce59a900
IMP/Util distinguishes between sets and functions again; imported only where used.

diff -r eda112e9cdee -r b4b5cbca2519 src/HOL/IMP/HoareT.thy
--- 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
diff -r eda112e9cdee -r b4b5cbca2519 src/HOL/IMP/Hoare_Examples.thy
--- 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 *}
 
diff -r eda112e9cdee -r b4b5cbca2519 src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
--- 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"
diff -r eda112e9cdee -r b4b5cbca2519 src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
--- 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"
diff -r eda112e9cdee -r b4b5cbca2519 src/HOL/IMP/Procs_Stat_Vars_Stat.thy
--- 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"
diff -r eda112e9cdee -r b4b5cbca2519 src/HOL/IMP/Util.thy
--- 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.
 *}