changeset 12441 | c586d08520ad |
parent 11070 | cc421547e744 |
child 12520 | 6d754b9a1303 |
--- a/src/HOL/MicroJava/ROOT.ML Mon Dec 10 15:23:19 2001 +0100 +++ b/src/HOL/MicroJava/ROOT.ML Mon Dec 10 15:24:22 2001 +0100 @@ -6,6 +6,8 @@ use_thy "JTypeSafe"; use_thy "Example"; +use_thy "JListExample"; +use_thy "JVMListExample"; use_thy "BVSpecTypeSafe"; use_thy "LBVCorrect"; use_thy "LBVComplete";