| changeset 6309 | ca52347e259a |
| parent 6299 | 1a88db6e7c7e |
| child 6536 | 281d44905cab |
| 6308:76f3865a2b1d | 6309:ca52347e259a |
|---|---|
5 |
5 |
6 Unions of programs |
6 Unions of programs |
7 |
7 |
8 From Misra's Chapter 5: Asynchronous Compositions of Programs |
8 From Misra's Chapter 5: Asynchronous Compositions of Programs |
9 *) |
9 *) |
10 |
|
11 |
|
12 Goal "k:I ==> (INT i:I. A i) Int A k = (INT i:I. A i)"; |
|
13 by (Blast_tac 1); |
|
14 qed "INT_absorb2"; |
|
15 |
|
16 |
|
17 val rinst = read_instantiate_sg (sign_of thy); |
|
18 |
10 |
19 Addcongs [UN_cong, INT_cong]; |
11 Addcongs [UN_cong, INT_cong]; |
20 |
12 |
21 |
13 |
22 (** SKIP **) |
14 (** SKIP **) |