author | nipkow |
Mon, 30 Apr 2001 19:26:04 +0200 | |
changeset 11275 | 71498de45241 |
parent 10342 | b124d59f7b61 |
child 13095 | 8ed413a57bdc |
permissions | -rw-r--r-- |
9277 | 1 |
(* Title: HOL/IMP/ROOT.ML |
2 |
ID: $Id$ |
|
3 |
Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb |
|
4 |
Copyright 1995 TUM |
|
9276 | 5 |
|
6 |
Caveat: HOLCF/IMP depends on HOL/IMP |
|
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
7 |
*) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
8 |
|
1696 | 9 |
time_use_thy "Expr"; |
10 |
time_use_thy "Transition"; |
|
1447 | 11 |
time_use_thy "VC"; |
9241 | 12 |
time_use_thy "Examples"; |
10342 | 13 |
time_use_thy "Compiler"; |