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.
Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
authorhoelzl
Thu, 02 Sep 2010 21:08:31 +0200
changeset 39101 606432dd1896
parent 39100 e9467adb8b52
child 39104 7430f17fd80e
Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
src/HOL/Fun.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Fun.thy	Thu Sep 02 20:44:33 2010 +0200
+++ b/src/HOL/Fun.thy	Thu Sep 02 21:08:31 2010 +0200
@@ -177,7 +177,7 @@
 lemma surj_id[simp]: "surj_on id A"
 by (simp add: surj_on_def)
 
-lemma bij_id[simp]: "bij_betw id A A"
+lemma bij_id[simp]: "bij id"
 by (simp add: bij_betw_def)
 
 lemma inj_onI:
isabelle