equal
deleted
inserted
replaced
6 |
6 |
7 theory RPCMemoryParams |
7 theory RPCMemoryParams |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 types |
11 type_synonym bit = "bool" |
12 bit = "bool" (* Signal wires for the procedure interface. |
12 (* Signal wires for the procedure interface. |
13 Defined as bool for simplicity. All I should really need is |
13 Defined as bool for simplicity. All I should really need is |
14 the existence of two distinct values. *) |
14 the existence of two distinct values. *) |
15 |
15 |
16 (* all of these are simple (HOL) types *) |
16 (* all of these are simple (HOL) types *) |
17 typedecl Locs (* "syntactic" value type *) |
17 typedecl Locs (* "syntactic" value type *) |
18 typedecl Vals (* "syntactic" value type *) |
18 typedecl Vals (* "syntactic" value type *) |
19 typedecl PrIds (* process id's *) |
19 typedecl PrIds (* process id's *) |