changeset 12978 | 16cc829b9c65 |
parent 12951 | a9fdcb71d252 |
child 13062 | 4b1edf2f6bd2 |
--- a/src/HOL/MicroJava/ROOT.ML Thu Feb 28 18:11:11 2002 +0100 +++ b/src/HOL/MicroJava/ROOT.ML Thu Feb 28 18:16:23 2002 +0100 @@ -13,9 +13,9 @@ use_thy "JVM"; use_thy "BVSpecTypeSafe"; use_thy "BVExample"; +use_thy "LBVSpec"; (* momentarily broken: -use_thy "LBVSpec"; use_thy "LBVCorrect"; use_thy "LBVComplete"; *)