IOA/meta_theory/Solve.ML

 
   (* Show that it's an execution fragment *)
   by (asm_full_simp_tac (SS addsimps [is_execution_fragment_def])1);
   by (safe_tac HOL_cs);
 
-  (* Cases on whether action is external or not (basically) *)
-  (* 1 *)
-  by (eres_inst_tac [("x","snd(ex,n)")] allE 1);
-  by (eres_inst_tac [("x","snd(ex,Suc(n))")] allE 1);
-  by (eres_inst_tac [("x","aa")] allE 1);
-  by (asm_full_simp_tac SS 1);
-
-  (* 2 *)
   by (eres_inst_tac [("x","snd(ex,n)")] allE 1);
   by (eres_inst_tac [("x","snd(ex,Suc(n))")] allE 1);
   by (eres_inst_tac [("x","a")] allE 1);
   by (asm_full_simp_tac SS 1);
 qed "trace_inclusion";