# HG changeset patch
# User nipkow
# Date 791655480 -3600
# Node ID 408713c7f66bc5fdec21609eee6d33ad9796d0b6
# Parent  7b9a06035a92f09894d5c4801c4f2a1d5ad0c24f
Simplified proof.

diff -r 7b9a06035a92 -r 408713c7f66b IOA/meta_theory/Solve.ML
--- a/IOA/meta_theory/Solve.ML	Wed Feb 01 17:17:35 1995 +0100
+++ b/IOA/meta_theory/Solve.ML	Wed Feb 01 17:18:00 1995 +0100
@@ -38,14 +38,6 @@
   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);