Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/BV/LBVComplete.thy
changeset 9664 4cae97480a6d
parent 9594 42d11e0a7a8b
child 9757 1024a2d80ac0 
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Sat Aug 19 12:49:19 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Sun Aug 20 17:45:20 2000 +0200
@@ -282,7 +282,7 @@
                "G \<turnstile> s2 <=s s1" "i = ins!pc"
 
   show ?thesis
-  proof (cases "cert!pc")
+  proof (cases (open) "cert!pc")
     case None
     with wtl fits
     show ?thesis
isabelle