equal
deleted
inserted
replaced
3 Copyright 1999 University of Cambridge |
3 Copyright 1999 University of Cambridge |
4 |
4 |
5 lift_prog, etc: replication of components and arrays of processes. |
5 lift_prog, etc: replication of components and arrays of processes. |
6 *) |
6 *) |
7 |
7 |
8 header{*Replication of Components*} |
8 section{*Replication of Components*} |
9 |
9 |
10 theory Lift_prog imports Rename begin |
10 theory Lift_prog imports Rename begin |
11 |
11 |
12 definition insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)" where |
12 definition insert_map :: "[nat, 'b, nat=>'b] => (nat=>'b)" where |
13 "insert_map i z f k == if k<i then f k |
13 "insert_map i z f k == if k<i then f k |