equal
deleted
inserted
replaced
1 (* Title: HOLCF/IOA/ex/ROOT.ML |
1 (* Title: HOLCF/IOA/ex/ROOT.ML |
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
2 Author: Olaf Mueller |
4 *) |
3 *) |
5 |
4 |
6 time_use_thy "TrivEx"; |
5 use_thys ["TrivEx", "TrivEx2"]; |
7 time_use_thy "TrivEx2"; |
|