src/HOLCF/IOA/meta_theory/Deadlock.thy
changeset 26359 6d437bde2f1d
parent 19741 f65265d71426
child 27208 5fe899199f85
--- a/src/HOLCF/IOA/meta_theory/Deadlock.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -15,7 +15,7 @@
   "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|]  
           ==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A"
 apply (simp add: schedules_def has_schedule_def)
-apply (tactic "safe_tac set_cs")
+apply auto
 apply (frule inp_is_act)
 apply (simp add: executions_def)
 apply (tactic {* pair_tac "ex" 1 *})