equal
deleted
inserted
replaced
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 "Pointers0"; |
8 time_use_thy "Pointers0"; |
9 time_use_thy "Pointers"; |
9 time_use_thy "Pointer_Examples"; |