| changeset 9277 | a0a7c31cdc39 |
| parent 9276 | 9e619ac0fe2f |
| child 10342 | b124d59f7b61 |
| 9276:9e619ac0fe2f | 9277:a0a7c31cdc39 |
|---|---|
1 (* Title: HOL/IMP/ROOT.ML |
1 (* Title: HOL/IMP/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow |
3 Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb |
4 Copyright 1995 TUM |
4 Copyright 1995 TUM |
5 |
5 |
6 Caveat: HOLCF/IMP depends on HOL/IMP |
6 Caveat: HOLCF/IMP depends on HOL/IMP |
7 *) |
7 *) |
8 |
8 |
9 time_use_thy "Expr"; |
9 time_use_thy "Expr"; |