equal
deleted
inserted
replaced
1 (* Title: HOL/Lex/ROOT.ML |
1 (* Title: HOL/Lex/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
6 |
|
7 HOL_build_completed; (*Make examples fail if HOL did*) |
|
8 |
6 |
9 use_thy"AutoChopper"; |
7 use_thy"AutoChopper"; |
10 use_thy"AutoChopper1"; |
8 use_thy"AutoChopper1"; |
11 use_thy"AutoMaxChop"; |
9 use_thy"AutoMaxChop"; |
12 (* Do not swap the next two use_thy's. |
10 (* Do not swap the next two use_thy's. |