author | nipkow |
Wed, 14 May 2003 14:20:55 +0200 | |
changeset 14028 | ff6eb32b30a1 |
parent 13875 | 12997e3ddd8d |
child 24104 | 719fbe4fb77f |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/IMP/ROOT.ML |
1335 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
14028 | 4 |
Copyright 1998-2003 TUM |
1335 | 5 |
*) |
6 |
||
9000 | 7 |
time_use_thy "Examples"; |
13857 | 8 |
time_use_thy "ExamplesAbort"; |
13771 | 9 |
time_use_thy "Pointers0"; |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
13771
diff
changeset
|
10 |
time_use_thy "Pointer_Examples"; |
13875 | 11 |
time_use_thy "Pointer_ExamplesAbort"; |
12 |
time_use_thy "SchorrWaite"; |
|
14028 | 13 |
time_use_thy "Separation"; |