# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1476366195 -7200
# Node ID 4d1d2de432fa666a35af86931e2abbf2cf9062b4
# Parent  676763a9c269a4245aeb751042d44173f0f46728
renamed lemma to a more consistent name

diff -r 676763a9c269 -r 4d1d2de432fa src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Thu Oct 13 14:41:45 2016 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Thu Oct 13 15:43:15 2016 +0200
@@ -582,7 +582,7 @@
 lemma fmrel_on_fset_alt_def: "fmrel_on_fset S P m n \<longleftrightarrow> fBall S (\<lambda>x. rel_option P (fmlookup m x) (fmlookup n x))"
 by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def)
 
-lemma rel_map_on_fsetI[intro]:
+lemma fmrel_on_fsetI[intro]:
   assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
   shows "fmrel_on_fset S P m n"
 using assms