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/Effect.thy
changeset 18576 8d98b7711e47
parent 18447 da548623916a
child 25362 8d06e11a01d1 
--- a/src/HOL/MicroJava/BV/Effect.thy	Wed Jan 04 17:04:11 2006 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Jan 04 19:22:53 2006 +0100
@@ -208,8 +208,7 @@
   "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow> 
   \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
   apply (cases i)
-  apply (auto iff: not_None_eq
-	      dest!: match_any_match_table match_X_match_table 
+  apply (auto dest!: match_any_match_table match_X_match_table 
               dest: match_exception_table_in_et)
   done
isabelle