equal
deleted
inserted
replaced
1 (* Title: HOL/IMP/ROOT.ML |
1 (* Title: HOL/IMP/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998-2003 TUM |
5 *) |
5 *) |
6 |
6 |
7 time_use_thy "Examples"; |
7 time_use_thy "Examples"; |
8 time_use_thy "ExamplesAbort"; |
8 time_use_thy "ExamplesAbort"; |
9 time_use_thy "Pointers0"; |
9 time_use_thy "Pointers0"; |
10 time_use_thy "Pointer_Examples"; |
10 time_use_thy "Pointer_Examples"; |
11 time_use_thy "Pointer_ExamplesAbort"; |
11 time_use_thy "Pointer_ExamplesAbort"; |
12 time_use_thy "SchorrWaite"; |
12 time_use_thy "SchorrWaite"; |
|
13 time_use_thy "Separation"; |