# HG changeset patch
# User nipkow
# Date 1352046986 -3600
# Node ID 0130ad32a61226a6bcf22b8cb885d711a04bded5
# Parent  e9a9bff107da223712719cd9bed53b19f3d8d5e6
now that sets are executable again, no more special treatment of variable sets

diff -r e9a9bff107da -r 0130ad32a612 src/HOL/IMP/Vars.thy
--- 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
-