changeset 17087 | 0abf74bdf712 |
parent 16417 | 9bc16273c2d4 |
child 17090 | 603f23d71ada |
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Tue Aug 16 19:25:32 2005 +0200 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy Tue Aug 16 19:25:42 2005 +0200 @@ -27,7 +27,7 @@ lemma [code]: "is_target step phi pc' = list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]" - apply (simp add: list_ex_def is_target_def set_mem_eq) + apply (simp add: list_ex_def is_target_def mem_iff) apply force done