equal
deleted
inserted
replaced
3 theory Util imports Main |
3 theory Util imports Main |
4 begin |
4 begin |
5 |
5 |
6 subsection "Show sets of variables as lists" |
6 subsection "Show sets of variables as lists" |
7 |
7 |
8 text {* Sets are functions and are not displayed by element if |
8 text {* Sets may be infinite and are not always displayed by element |
9 computed as values: *} |
9 if computed as values. Lists do not have this problem. |
10 value "{''x'', ''y''}" |
|
11 |
10 |
12 text {* Lists do not have this problem *} |
11 We define a function @{text show} that converts a set of |
13 value "[''x'', ''y'']" |
|
14 |
|
15 text {* We define a function @{text show} that converts a set of |
|
16 variable names into a list. To keep things simple, we rely on |
12 variable names into a list. To keep things simple, we rely on |
17 the convention that we only use single letter names. |
13 the convention that we only use single letter names. |
18 *} |
14 *} |
19 definition |
15 definition |
20 letters :: "string list" where |
16 letters :: "string list" where |