Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SizeChange/Correctness.thy
changeset 32988 d1d4d7a08a66
parent 31979 09f65e860bdb
child 32989 c28279b29ff1 
--- a/src/HOL/SizeChange/Correctness.thy	Sat Oct 17 13:46:55 2009 +0200
+++ b/src/HOL/SizeChange/Correctness.thy	Sun Oct 18 12:07:25 2009 +0200
@@ -1147,7 +1147,7 @@
   assumes "finite S" 
   shows "set (set2list S) = S"
   unfolding set2list_def 
-proof (rule f_inv_f)
+proof (rule f_inv_onto_f)
   from `finite S` have "\<exists>l. set l = S"
     by (rule finite_list)
   thus "S \<in> range set"
isabelle