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.
tuned proof;
authorwenzelm
Tue, 02 Aug 2016 22:36:53 +0200
changeset 63591 8d20875f1290
parent 63590 4854f7ee0987
child 63592 64db21931bcb
tuned proof;
src/HOL/Fun.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Fun.thy	Tue Aug 02 21:55:15 2016 +0200
+++ b/src/HOL/Fun.thy	Tue Aug 02 22:36:53 2016 +0200
@@ -411,7 +411,7 @@
 qed
 
 lemma bij_betw_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
-  unfolding bij_betw_def inj_on_def by force  (* slow *)
+  unfolding bij_betw_def inj_on_def by safe force+  (* somewhat slow *)
 
 lemma bij_betw_id[intro, simp]: "bij_betw id A A"
   unfolding bij_betw_def id_def by auto
isabelle