# HG changeset patch # User Lars Hupel # 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 \ fBall S (\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 "\x. x |\| S \ rel_option P (fmlookup m x) (fmlookup n x)" shows "fmrel_on_fset S P m n" using assms