equal
deleted
inserted
replaced
7 Strictly speaking a shallow embedding (as implemented by Norbert Galm |
7 Strictly speaking a shallow embedding (as implemented by Norbert Galm |
8 following Mike Gordon) would suffice. Maybe the datatype com comes in useful |
8 following Mike Gordon) would suffice. Maybe the datatype com comes in useful |
9 later. |
9 later. |
10 *) |
10 *) |
11 |
11 |
12 theory Hoare = Main |
12 theory Hoare imports Main |
13 files ("hoare.ML"): |
13 uses ("hoare.ML") begin |
14 |
14 |
15 types |
15 types |
16 'a bexp = "'a set" |
16 'a bexp = "'a set" |
17 'a assn = "'a set" |
17 'a assn = "'a set" |
18 |
18 |