| changeset 168 | 44ff2275d44f |
| parent 156 | fd1be45b64bf |
| child 171 | 16c4ea954511 |
| 167:37a6e2f55230 | 168:44ff2275d44f |
|---|---|
1 (* Title: HOL/IOA/example/Impl.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 The implementation --- Invariants |
|
7 *) |
|
8 |
|
1 val impl_ioas = |
9 val impl_ioas = |
2 [Impl.impl_def, |
10 [Impl.impl_def, |
3 Sender.sender_ioa_def, |
11 Sender.sender_ioa_def, |
4 Receiver.receiver_ioa_def, |
12 Receiver.receiver_ioa_def, |
5 Channels.srch_ioa_def, |
13 Channels.srch_ioa_def, |