# HG changeset patch
# User nipkow
# Date 1124213142 -7200
# Node ID 0abf74bdf71224affe595b2648c5c482fb4a0261
# Parent  0eb0c9259dd77ad81fff18750316020a515af039
name fix

diff -r 0eb0c9259dd7 -r 0abf74bdf712 src/HOL/Auth/Guard/Guard.thy
--- 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)
diff -r 0eb0c9259dd7 -r 0abf74bdf712 src/HOL/Auth/Guard/GuardK.thy
--- 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)
diff -r 0eb0c9259dd7 -r 0abf74bdf712 src/HOL/MicroJava/BV/LBVComplete.thy
--- 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