Mercurial Mercurial > repos > isabelle / 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.
proof can be shortened now
authorpaulson
Wed, 21 Aug 2002 15:55:59 +0200
changeset 13510 0a0f37f9c031
parent 13509 6f168374652a
child 13511 e4b129eaa9c6
proof can be shortened now
src/ZF/UNITY/GenPrefix.ML file | annotate | diff | comparison | revisions 
--- a/src/ZF/UNITY/GenPrefix.ML	Wed Aug 21 15:55:40 2002 +0200
+++ b/src/ZF/UNITY/GenPrefix.ML	Wed Aug 21 15:55:59 2002 +0200
@@ -305,9 +305,6 @@
 by (ALLGOALS(Asm_full_simp_tac));
 by (etac natE 1);
 by (ALLGOALS(Asm_full_simp_tac));
-by (dres_inst_tac [("x", "ysa")] bspec 1);
-by (dres_inst_tac [("x", "x")] bspec 2);
-by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset()));
 qed_spec_mp "gen_prefix_imp_nth";
 
 Goal "xs:list(A) ==> \
isabelle