--- a/src/HOL/Fun.thy Thu Jul 28 20:39:51 2016 +0200
+++ b/src/HOL/Fun.thy Fri Jul 29 09:49:23 2016 +0200
@@ -666,6 +666,12 @@
lemma override_on_apply_in[simp]: "a \<in> A \<Longrightarrow> (override_on f g A) a = g a"
by (simp add:override_on_def)
+lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)"
+unfolding override_on_def by (simp add: fun_eq_iff)
+
+lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)"
+unfolding override_on_def by (simp add: fun_eq_iff)
+
subsection \<open>\<open>swap\<close>\<close>