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.
adapted proof of finite_converse
authoroheimb
Mon, 30 Mar 1998 21:09:46 +0200
changeset 4763 56072b72d730
parent 4762 afebaa81f148
child 4764 9b3293646b5d
adapted proof of finite_converse
src/HOL/Finite.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Finite.ML	Mon Mar 30 21:08:05 1998 +0200
+++ b/src/HOL/Finite.ML	Mon Mar 30 21:09:46 1998 +0200
@@ -195,9 +195,7 @@
 by Auto_tac;
  by (rtac bexI 1);
  by (assume_tac 2);
- by (Simp_tac 1);
-by (split_all_tac 1);
-by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
 qed "finite_converse";
 AddIffs [finite_converse];
isabelle