Mod due to new thm in Map.
authornipkow
Mon, 15 Sep 2003 17:15:00 +0200
changeset 14191 2014eac694d2
parent 14190 609c072edf90
child 14192 d6cb80cc1d20
Mod due to new thm in Map.
src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Mon Sep 15 14:00:43 2003 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Mon Sep 15 17:15:00 2003 +0200
@@ -198,7 +198,6 @@
   apply clarify  
   apply simp
   apply (rule conjI) 
-   apply (simp add: nth_list_update)
    apply blast
   apply (simp add: nth_list_update)
   apply blast
@@ -471,4 +470,4 @@
 apply (blast intro!: le_listD less_lengthI)
 done
 
-end
\ No newline at end of file
+end