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/Fun.thy
changeset 62390 842917225d56
parent 61955 e96292f32c3c
child 62618 f7f2467ab854 
--- a/src/HOL/Fun.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Fun.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -667,7 +667,7 @@
   by auto
 
 lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z"
-by(simp add: fun_eq_iff split: split_if_asm)
+by(simp add: fun_eq_iff split: if_split_asm)
 
 subsection \<open>\<open>override_on\<close>\<close>
isabelle