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.
this change saves 15 seconds
authorpaulson
Sun, 23 Apr 2000 11:39:32 +0200
changeset 8767 eae30939b592
parent 8766 1ef6e77e12ee
child 8768 9f18aba48519
this change saves 15 seconds
src/HOL/Fun.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Fun.ML	Sun Apr 23 11:35:00 2000 +0200
+++ b/src/HOL/Fun.ML	Sun Apr 23 11:39:32 2000 +0200
@@ -406,7 +406,7 @@
 qed "bij_image_Collect_eq";
 
 Goal "bij f ==> f -`` A = inv f `` A";
-by Auto_tac;
+by Safe_tac;
 by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
 by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
 qed "bij_vimage_eq_inv_image";
isabelle