src/HOL/Lifting_Set.thy
changeset 63040 eb4ddd18d635
parent 62343 24106dc44def
child 63343 fb5d8a50c641
     1.1 --- a/src/HOL/Lifting_Set.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4    assumes "bi_unique R" and "rel_set R X Y"
     1.5    obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)"
     1.6  proof
     1.7 -  def f \<equiv> "\<lambda>x. THE y. R x y"
     1.8 +  define f where "f x = (THE y. R x y)" for x
     1.9    { fix x assume "x \<in> X"
    1.10      with \<open>rel_set R X Y\<close> \<open>bi_unique R\<close> have "R x (f x)"
    1.11        by (simp add: bi_unique_def rel_set_def f_def) (metis theI)