equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 Rename = Extend + |
9 Rename = Extend + |
10 |
10 |
11 constdefs |
11 constdefs |
12 rename_act :: "['a => 'b, ('a*'a) set] => ('b*'b) set" |
|
13 "rename_act h == extend_act (%(x,u::unit). h x)" |
|
14 |
|
15 (**OR |
|
16 "rename_act h == %act. UN (s,s'): act. {(h s, h s')}" |
|
17 "rename_act h == %act. (prod_fun h h) `` act" |
|
18 **) |
|
19 |
12 |
20 rename :: "['a => 'b, 'a program] => 'b program" |
13 rename :: "['a => 'b, 'a program] => 'b program" |
21 "rename h == extend (%(x,u::unit). h x)" |
14 "rename h == extend (%(x,u::unit). h x)" |
22 |
15 |
23 end |
16 end |