src/ZF/Constructible/Datatype_absolute.thy
changeset 13293 09276ee04361
parent 13269 3ba9be497c33
child 13306 6eebcddee32b
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 04 10:53:52 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 04 10:54:04 2002 +0200
     1.3 @@ -138,10 +138,10 @@
     1.4  lemma (in M_datatypes) list_replacement1':
     1.5    "[|M(A); n \<in> nat|]
     1.6     ==> strong_replacement
     1.7 -	  (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x,z\<rangle> &
     1.8 -               is_recfun (Memrel(succ(n)), x,
     1.9 +	  (M, \<lambda>x y. \<exists>z[M]. y = \<langle>x,z\<rangle> &
    1.10 +               (\<exists>g[M]. is_recfun (Memrel(succ(n)), x,
    1.11  		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
    1.12 - 	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))"
    1.13 + 	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x)))"
    1.14  by (insert list_replacement1, simp add: nat_into_M) 
    1.15  
    1.16  
    1.17 @@ -149,4 +149,5 @@
    1.18       "M(A) ==> M(list(A))"
    1.19  by (simp add: list_eq_Union list_replacement1' list_replacement2')
    1.20  
    1.21 +
    1.22  end