# HG changeset patch # User kleing # Date 1017258303 -3600 # Node ID 0e028b1f3f38d77ecafa624d21643af1dce64a2f # Parent f538a1dba7ee41ad5eea4edc0be0f2a5bd9dd378 added lbv completeness diff -r f538a1dba7ee -r 0e028b1f3f38 src/HOL/MicroJava/ROOT.ML --- a/src/HOL/MicroJava/ROOT.ML Wed Mar 27 20:44:53 2002 +0100 +++ b/src/HOL/MicroJava/ROOT.ML Wed Mar 27 20:45:03 2002 +0100 @@ -14,7 +14,4 @@ use_thy "BVSpecTypeSafe"; use_thy "BVExample"; use_thy "LBVCorrect"; - -(* momentarily broken: use_thy "LBVComplete"; -*)