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