src/HOL/Wfrec.thy
changeset 63040 eb4ddd18d635
parent 61799 4cf66f21b764
child 63572 c0cbfd2b5a45
     1.1 --- a/src/HOL/Wfrec.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/Wfrec.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  lemma wfrec_unique: assumes "adm_wf R F" "wf R" shows "\<exists>!y. wfrec_rel R F x y"
     1.5    using \<open>wf R\<close>
     1.6  proof induct
     1.7 -  def f \<equiv> "\<lambda>y. THE z. wfrec_rel R F y z"
     1.8 +  define f where "f y = (THE z. wfrec_rel R F y z)" for y
     1.9    case (less x)
    1.10    then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y"
    1.11      unfolding f_def by (rule theI_unique)