--- 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