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 *})