src/HOL/HOLCF/Adm.thy
changeset 63040 eb4ddd18d635
parent 62175 8ffc4d0e652d
child 67312 0d25e02759b7
     1.1 --- a/src/HOL/HOLCF/Adm.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/HOLCF/Adm.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -61,7 +61,7 @@
     1.4    assumes P: "\<forall>i. \<exists>j\<ge>i. P (Y j)"
     1.5    shows "P (\<Squnion>i. Y i)"
     1.6  proof -
     1.7 -  def f \<equiv> "\<lambda>i. LEAST j. i \<le> j \<and> P (Y j)"
     1.8 +  define f where "f i = (LEAST j. i \<le> j \<and> P (Y j))" for i
     1.9    have chain': "chain (\<lambda>i. Y (f i))"
    1.10      unfolding f_def
    1.11      apply (rule chainI)