changeset 62195 | 799a5306e2ed |
parent 62156 | 7355fd313cf8 |
child 62390 | 842917225d56 |
--- a/src/HOL/HOLCF/IOA/Deadlock.thy Sat Jan 16 23:35:55 2016 +0100 +++ b/src/HOL/HOLCF/IOA/Deadlock.thy Sun Jan 17 00:14:45 2016 +0100 @@ -17,7 +17,7 @@ apply auto apply (frule inp_is_act) apply (simp add: executions_def) - apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) + apply (pair ex) apply (rename_tac s ex) apply (subgoal_tac "Finite ex") prefer 2