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/Library/Nat_Bijection.thy
changeset 51489 f738e6dbd844
parent 51414 587f493447d9
child 57512 cc97b347b301 
--- a/src/HOL/Library/Nat_Bijection.thy	Sat Mar 23 17:11:06 2013 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy	Sat Mar 23 20:50:39 2013 +0100
@@ -377,7 +377,7 @@
       by (metis finite_set_decode set_decode_inverse)
   thus ?thesis using assms
     apply auto
-    apply (simp add: set_encode_def nat_add_commute setsum.F_subset_diff)
+    apply (simp add: set_encode_def nat_add_commute setsum.subset_diff)
     done
   qed
   thus ?thesis
@@ -385,3 +385,4 @@
 qed
 
 end
+
isabelle