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/Bali/AxCompl.thy
changeset 46714 a7ca72710dfe
parent 45605 a89b4bc311a5
child 48001 c79adcae9869 
--- a/src/HOL/Bali/AxCompl.thy	Mon Feb 27 17:39:34 2012 +0100
+++ b/src/HOL/Bali/AxCompl.thy	Mon Feb 27 17:40:59 2012 +0100
@@ -1299,7 +1299,7 @@
         apply -
         apply (rule MGFn_NormalI)
         apply (rule ax_derivs.Jmp [THEN conseq1])
-        apply (auto intro: eval.Jmp simp add: abupd_def2)
+        apply (auto intro: eval.Jmp)
         done
     next
       case (Throw e)
isabelle