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/Kildall.thy
changeset 13601 fd3e3d6b37b2
parent 13074 96bf406fd3e5
child 14191 2014eac694d2 
--- a/src/HOL/MicroJava/BV/Kildall.thy	Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Mon Sep 30 16:14:02 2002 +0200
@@ -136,12 +136,9 @@
        apply (blast dest: boundedD)
       apply blast
    apply clarify
-   apply (rotate_tac -2)
    apply (erule allE)
    apply (erule impE)
     apply assumption
-   apply (erule impE)
-    apply assumption
    apply (drule bspec)
     apply assumption
    apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
@@ -435,7 +432,6 @@
 defer
 apply assumption
 apply clarsimp
-apply (blast dest!: boundedD)
 done
isabelle