--- a/src/HOL/Auth/Guard/Guard.thy Tue Aug 16 19:25:32 2005 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy Tue Aug 16 19:25:42 2005 +0200
@@ -274,7 +274,7 @@
apply (clarsimp, blast)
(* K ~:invKey`Ks *)
apply (subgoal_tac "Guard n Ks (set (decrypt' l' K Y))")
-apply (drule_tac x="decrypt' l' K Y" in spec, simp add: set_mem_eq)
+apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
apply (subgoal_tac "Crypt K Y:parts (set l)")
apply (drule parts_cnb, rotate_tac -1, simp)
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
--- a/src/HOL/Auth/Guard/GuardK.thy Tue Aug 16 19:25:32 2005 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy Tue Aug 16 19:25:42 2005 +0200
@@ -270,7 +270,7 @@
apply (clarsimp, blast)
(* K ~:invKey`Ks *)
apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))")
-apply (drule_tac x="decrypt' l' K Y" in spec, simp add: set_mem_eq)
+apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
apply (subgoal_tac "Crypt K Y:parts (set l)")
apply (drule parts_cnb, rotate_tac -1, simp)
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)
--- 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