Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
included LBVSpec again
authorkleing
Thu, 28 Feb 2002 18:16:23 +0100
changeset 12978 16cc829b9c65
parent 12977 fcc9a30a7ef2
child 12979 4c76bce4ce39
included LBVSpec again
src/HOL/MicroJava/BV/LBVSpec.thy file | annotate | diff | comparison | revisions
src/HOL/MicroJava/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Feb 28 18:11:11 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Feb 28 18:16:23 2002 +0100
@@ -15,7 +15,9 @@
   soundness and completeness are broken (they still need to be
   ported to the exception version). Both theories are included
   for documentation (but they don't work for this specification), 
-  please see the Isabelle 99-2 release for a working copy.
+  please see the Isabelle 99-2 release for a working copy, or
+  \url{http://isabelle.in.tum.de/verificard} for the most recent
+  development of \mJava.
 *}
 
 types
--- 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";
 *)
isabelle