--- a/src/HOL/MicroJava/BV/LBVSpec.thy Fri Aug 28 20:07:11 2009 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Fri Aug 28 20:18:33 2009 +0200
@@ -293,7 +293,7 @@
shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
proof -
from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
- with suc wtl show ?thesis by (simp add: min_def)
+ with suc wtl show ?thesis by (simp)
qed
lemma (in lbv) wtl_all:
@@ -308,7 +308,7 @@
with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp
from pc have "is!pc = drop pc is ! 0" by simp
with Cons have "is!pc = i" by simp
- with take pc show ?thesis by (auto simp add: min_def split: split_if_asm)
+ with take pc show ?thesis by (auto)
qed
section "preserves-type"