Mercurial Mercurial > repos > Old_HOL / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simplified proof.
authornipkow
Wed, 01 Feb 1995 17:18:00 +0100
changeset 207 408713c7f66b
parent 206 7b9a06035a92
child 208 deec279dda0a
Simplified proof.
IOA/meta_theory/Solve.ML file | annotate | diff | comparison | revisions 
--- 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