# HG changeset patch
# User wenzelm
# Date 1466437907 -7200
# Node ID 1e98146f3581ce9215180895604249eed992b1ab
# Parent  814541a57d89fd856fbaf96188105f556a822637
prefer HOL definitions;

diff -r 814541a57d89 -r 1e98146f3581 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Jun 20 17:25:08 2016 +0200
+++ b/src/HOL/Fun.thy	Mon Jun 20 17:51:47 2016 +0200
@@ -584,7 +584,7 @@
 subsection \<open>Function Updating\<close>
 
 definition fun_upd :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
-  where "fun_upd f a b \<equiv> \<lambda>x. if x = a then b else f x"
+  where "fun_upd f a b = (\<lambda>x. if x = a then b else f x)"
 
 nonterminal updbinds and updbind
 
@@ -739,7 +739,7 @@
 subsection \<open>Inversion of injective functions\<close>
 
 definition the_inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
-  where "the_inv_into A f \<equiv> \<lambda>x. THE y. y \<in> A \<and> f y = x"
+  where "the_inv_into A f = (\<lambda>x. THE y. y \<in> A \<and> f y = x)"
 
 lemma the_inv_into_f_f: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> the_inv_into A f (f x) = x"
   unfolding the_inv_into_def inj_on_def by blast