Mercurial Mercurial > repos > Old_HOL / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IOA/meta_theory/Solve.ML
changeset 207 408713c7f66b
parent 171 16c4ea954511 
--- 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);
Old_HOL