--- a/src/HOL/IMP/Vars.thy Fri Nov 02 16:16:48 2012 +0100
+++ b/src/HOL/IMP/Vars.thy Sun Nov 04 17:36:26 2012 +0100
@@ -5,25 +5,6 @@
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]) Enum.enum"
-
-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
@@ -52,10 +33,6 @@
value "vars(Plus (V ''x'') (V ''y''))"
-text{* We need to convert functions to lists before we can view them: *}
-
-value "show (vars(Plus (V ''x'') (V ''y'')))"
-
instantiation bexp :: vars
begin
@@ -91,4 +68,3 @@
qed simp_all
end
-