changeset 12338 | de0f4a63baa5 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
12337:7c6a970f0808 | 12338:de0f4a63baa5 |
---|---|
6 Refinement Mappings in HOLCF/IOA. |
6 Refinement Mappings in HOLCF/IOA. |
7 *) |
7 *) |
8 |
8 |
9 RefMappings = Traces + |
9 RefMappings = Traces + |
10 |
10 |
11 default term |
11 default type |
12 |
12 |
13 consts |
13 consts |
14 |
14 |
15 move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" |
15 move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" |
16 is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
16 is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |