changeset 62195 | 799a5306e2ed |
parent 62156 | 7355fd313cf8 |
child 63549 | b0d31c7def86 |
--- a/src/HOL/HOLCF/IOA/ShortExecutions.thy Sat Jan 16 23:35:55 2016 +0100 +++ b/src/HOL/HOLCF/IOA/ShortExecutions.thy Sun Jan 17 00:14:45 2016 +0100 @@ -212,7 +212,7 @@ apply auto apply (rule_tac x = "filter_act $ (Cut (\<lambda>a. fst a \<in> ext A) (snd ex))" in exI) apply (simp add: executions_def) - apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) + apply (pair ex) apply auto apply (rule_tac x = "(x1, Cut (\<lambda>a. fst a \<in> ext A) x2)" in exI) apply simp