| changeset 12522 | 69971d68fe03 |
| parent 12520 | 6d754b9a1303 |
| child 12773 | a47f51daa6dc |
--- a/src/HOL/MicroJava/ROOT.ML Sun Dec 16 00:20:17 2001 +0100 +++ b/src/HOL/MicroJava/ROOT.ML Mon Dec 17 13:25:18 2001 +0100 @@ -7,7 +7,7 @@ use_thy "JTypeSafe"; use_thy "Example"; use_thy "JListExample"; -(* use_thy "JVMListExample"; *) +use_thy "JVMListExample"; use_thy "BVSpecTypeSafe"; use_thy "JVM"; use_thy "LBVSpec";