src/HOL/Library/Finite_Map.thy
changeset 64181 4d1d2de432fa
parent 64180 676763a9c269
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Library/Finite_Map.thy	Thu Oct 13 14:41:45 2016 +0200
     1.2 +++ b/src/HOL/Library/Finite_Map.thy	Thu Oct 13 15:43:15 2016 +0200
     1.3 @@ -582,7 +582,7 @@
     1.4  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))"
     1.5  by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def)
     1.6  
     1.7 -lemma rel_map_on_fsetI[intro]:
     1.8 +lemma fmrel_on_fsetI[intro]:
     1.9    assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
    1.10    shows "fmrel_on_fset S P m n"
    1.11  using assms