diff -r dc39832e9280 -r 60a0f9caa0a2 src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Tue Jan 03 15:43:54 2006 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Tue Jan 03 15:44:39 2006 +0100
@@ -11,7 +11,7 @@
 
 header {*Extensions to Standard Theories*}
 
-theory Extensions imports Event begin
+theory Extensions imports "../Event" begin
 
 subsection{*Extensions to Theory @{text Set}*}
 
@@ -279,8 +279,8 @@
 analz (G Un H) = H - keysfor G Un (analz (G Un (H Int keysfor G)))"
 apply (rule eq)
 apply (erule analz.induct, blast)
-apply (simp, blast dest: Un_upper1)
-apply (simp, blast dest: Un_upper2)
+apply (simp, blast)
+apply (simp, blast)
 apply (case_tac "Key (invKey K):H - keysfor G", clarsimp)
 apply (drule_tac X=X in no_key_no_Crypt)
 by (auto intro: analz_sub)
@@ -587,7 +587,7 @@
 
 lemma known_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
 ==> X:parts (knows A evs) --> X:used evs"
-apply (case_tac "A=Spy", blast dest: parts_knows_Spy_subset_used)
+apply (case_tac "A=Spy", blast)
 apply (induct evs)
 apply (simp add: used.simps, blast)
 apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
@@ -600,7 +600,7 @@
 lemma known_max_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
 ==> X:parts (knows_max A evs) --> X:used evs"
 apply (case_tac "A=Spy")
-apply (simp, blast dest: parts_knows_Spy_subset_used)
+apply force
 apply (induct evs)
 apply (simp add: knows_max_def used.simps, blast)
 apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)