--- a/src/HOL/UNITY/Comp/Alloc.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Wed Feb 17 21:51:56 2016 +0100
@@ -1035,7 +1035,7 @@
apply (simp only: o_apply sub_def)
apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I])
apply (simp add: o_def del: INT_iff)
- apply (erule component_guaranteesD)
+ apply (drule component_guaranteesD)
apply (auto simp add:
System_Increasing_allocRel [simplified sub_apply o_def]
System_Increasing_allocAsk [simplified sub_apply o_def]
@@ -1047,6 +1047,7 @@
lemma System_Progress: "System : system_progress"
apply (unfold system_progress_def)
apply (cut_tac System_Alloc_Progress)
+ apply auto
apply (blast intro: LeadsTo_Trans
System_Follows_allocGiv [THEN Follows_LeadsTo_pfixLe]
System_Follows_ask [THEN Follows_LeadsTo])