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.
tuned proof;
authorwenzelm
Fri, 23 Sep 2011 21:51:49 +0200
changeset 45068 3cc2ac688fd9
parent 45067 d5156aa8556d
child 45069 981098cdbb3f
tuned proof;
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Sep 23 17:35:06 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Sep 23 21:51:49 2011 +0200
@@ -347,7 +347,7 @@
     from some_handler xp'
     have state': 
       "state' = (None, hp, ([xcp], loc, C, sig, handler)#frs)"
-      by (cases "ins!pc", auto simp add: raise_system_xcpt_def split_beta 
+      by (cases "ins!pc") (auto simp add: raise_system_xcpt_def split_beta 
                                split: split_if_asm) (* takes long! *)
 
     let ?f' = "([xcp], loc, C, sig, handler)"
isabelle