changeset 24106 | f2965bf954dc |
parent 12600 | 30ec65eaaf5f |
child 26438 | 090ced251009 |
24105:af364e2b4048 | 24106:f2965bf954dc |
---|---|
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1997 TU Muenchen |
4 Copyright 1997 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 with_path "../../HOL/IMP" (no_document time_use_thy) "Natural"; |
7 use_thys ["../../HOL/IMP/Natural", "HoareEx"]; |
8 time_use_thy "HoareEx"; |
|
9 |