# HG changeset patch
# User nipkow
# Date 1322769136 -3600
# Node ID ccf2cbe86d708534f98c421b3a08dcd7c8185337
# Parent  efd2b952f42588a4fe5bd0cd9682beeb318d413b
merged IMP/Util into IMP/Vars

diff -r efd2b952f425 -r ccf2cbe86d70 src/HOL/IMP/Util.thy
--- a/src/HOL/IMP/Util.thy	Thu Dec 01 15:41:58 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Util imports Main
-begin
-
-subsection "Show sets of variables as lists"
-
-text {* Sets may be infinite and are not always displayed by element 
-  if computed as values. Lists do not have this problem. 
-
-  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.
-*}
-definition 
-  letters :: "string list" where
-  "letters = map (\<lambda>c. [c]) chars"
-
-definition 
-  "show" :: "string set \<Rightarrow> string list" where
-  "show S = filter (\<lambda>x. x \<in> S) letters" 
-
-value "show {''x'', ''z''}"
-
-end
diff -r efd2b952f425 -r ccf2cbe86d70 src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Thu Dec 01 15:41:58 2011 +0100
+++ b/src/HOL/IMP/Vars.thy	Thu Dec 01 20:52:16 2011 +0100
@@ -2,9 +2,28 @@
 
 header "Definite Assignment Analysis"
 
-theory Vars imports Util BExp
+theory Vars imports BExp
 begin
 
+subsection "Show sets of variables as lists"
+
+text {* Sets may be infinite and are not always displayed by element 
+  if computed as values. Lists do not have this problem. 
+
+  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.
+*}
+definition 
+  letters :: "string list" where
+  "letters = map (\<lambda>c. [c]) chars"
+
+definition 
+  "show" :: "string set \<Rightarrow> string list" where
+  "show S = filter (\<lambda>x. x \<in> S) letters" 
+
+value "show {''x'', ''z''}"
+
 subsection "The Variables in an Expression"
 
 text{* We need to collect the variables in both arithmetic and boolean
diff -r efd2b952f425 -r ccf2cbe86d70 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Dec 01 15:41:58 2011 +0100
+++ b/src/HOL/IsaMakefile	Thu Dec 01 20:52:16 2011 +0100
@@ -530,7 +530,7 @@
   IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \
   IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \
   IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \
-  IMP/Util.thy IMP/VC.thy IMP/Vars.thy \
+  IMP/VC.thy IMP/Vars.thy \
   IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
 	@cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP