src/HOL/IMP/Util.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 44177 b4b5cbca2519
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Util imports Main
     4 begin
     5 
     6 subsection "Show sets of variables as lists"
     7 
     8 text {* Sets may be infinite and are not always displayed by element 
     9   if computed as values. Lists do not have this problem. 
    10 
    11   We define a function @{text show} that converts a set of
    12   variable names into a list. To keep things simple, we rely on
    13   the convention that we only use single letter names.
    14 *}
    15 definition 
    16   letters :: "string list" where
    17   "letters = map (\<lambda>c. [c]) chars"
    18 
    19 definition 
    20   "show" :: "string set \<Rightarrow> string list" where
    21   "show S = filter (\<lambda>x. x \<in> S) letters" 
    22 
    23 value "show {''x'', ''z''}"
    24 
    25 end