equal
deleted
inserted
replaced
16 ==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A" |
16 ==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A" |
17 apply (simp add: schedules_def has_schedule_def) |
17 apply (simp add: schedules_def has_schedule_def) |
18 apply auto |
18 apply auto |
19 apply (frule inp_is_act) |
19 apply (frule inp_is_act) |
20 apply (simp add: executions_def) |
20 apply (simp add: executions_def) |
21 apply (tactic {* pair_tac "ex" 1 *}) |
21 apply (tactic {* pair_tac @{context} "ex" 1 *}) |
22 apply (rename_tac s ex) |
22 apply (rename_tac s ex) |
23 apply (subgoal_tac "Finite ex") |
23 apply (subgoal_tac "Finite ex") |
24 prefer 2 |
24 prefer 2 |
25 apply (simp add: filter_act_def) |
25 apply (simp add: filter_act_def) |
26 defer |
26 defer |