--- a/src/HOL/Auth/Public.thy Thu Sep 09 14:38:14 2010 +0200
+++ b/src/HOL/Auth/Public.thy Thu Sep 09 16:47:03 2010 +0100
@@ -235,12 +235,10 @@
"\<forall>X \<in> used evs. parts {X} \<subseteq> used evs"
apply (induct evs)
prefer 2
- apply (simp add: used_Cons)
- apply (rule ballI)
- apply (case_tac a, auto)
-apply (auto dest!: parts_cut)
+ apply (simp add: used_Cons split: event.split)
+ apply (metis Un_iff empty_subsetI insert_subset le_supI1 le_supI2 parts_subset_iff)
txt{*Base case*}
-apply (simp add: used_Nil)
+apply (auto dest!: parts_cut simp add: used_Nil)
done
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H"