--- a/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy Wed Dec 25 17:39:06 2013 +0100
@@ -283,7 +283,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_max.inf_absorb2)
+ with suc wtl show ?thesis by (simp add: min.absorb2)
qed
lemma (in lbv) wtl_all:
@@ -298,7 +298,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_max.inf_absorb2)
+ with take pc show ?thesis by (auto simp add: min.absorb2)
qed
section "preserves-type"