changeset 13857 | 11d7c5a8dbb7 |
parent 13772 | 73d041cc6a66 |
child 13875 | 12997e3ddd8d |
13856:f5d08c341216 | 13857:11d7c5a8dbb7 |
---|---|
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
6 |
6 |
7 time_use_thy "Examples"; |
7 time_use_thy "Examples"; |
8 time_use_thy "ExamplesAbort"; |
|
8 time_use_thy "Pointers0"; |
9 time_use_thy "Pointers0"; |
9 time_use_thy "Pointer_Examples"; |
10 time_use_thy "Pointer_Examples"; |