| changeset 16417 | 9bc16273c2d4 |
| parent 15976 | 44f615d1729b |
| child 35416 | d8d7d1b785af |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header{*Renaming of State Sets*} |
7 header{*Renaming of State Sets*} |
8 |
8 |
9 theory Rename = Extend: |
9 theory Rename imports Extend begin |
10 |
10 |
11 constdefs |
11 constdefs |
12 |
12 |
13 rename :: "['a => 'b, 'a program] => 'b program" |
13 rename :: "['a => 'b, 'a program] => 'b program" |
14 "rename h == extend (%(x,u::unit). h x)" |
14 "rename h == extend (%(x,u::unit). h x)" |