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/LBVCorrect.thy
changeset 9664 4cae97480a6d
parent 9580 d955914193e0
child 9757 1024a2d80ac0 
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Sat Aug 19 12:49:19 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Sun Aug 20 17:45:20 2000 +0200
@@ -47,7 +47,7 @@
   have "\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc 
      \<longrightarrow> (\<exists> phi. pc + length is < length phi \<and> fits_partial phi pc is G rT s0 s2 cert)"
     (is "?P is")
-  proof (induct "?P" "is")
+  proof (induct (open) ?P "is")
     case Nil
     show "?P []" by (simp add: fits_partial_def exists_list)
     case Cons
isabelle