src/ZF/Constructible/Datatype_absolute.thy
changeset 13702 c7cf8fa66534
parent 13687 22dce9134953
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Nov 08 10:28:29 2002 +0100
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Nov 08 10:34:40 2002 +0100
     1.3 @@ -980,7 +980,6 @@
     1.4               \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
     1.5  apply (simp add: relation2_def MH_def, clarify)
     1.6  apply (rule lambda_abs2)
     1.7 -apply (rule fr_lam_replace, assumption)
     1.8  apply (rule Relation1_formula_rec_case)
     1.9  apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed)
    1.10  done