equal
deleted
inserted
replaced
978 lemma (in Formula_Rec) MH_rel2: |
978 lemma (in Formula_Rec) MH_rel2: |
979 "relation2 (M, MH, |
979 "relation2 (M, MH, |
980 \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))" |
980 \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))" |
981 apply (simp add: relation2_def MH_def, clarify) |
981 apply (simp add: relation2_def MH_def, clarify) |
982 apply (rule lambda_abs2) |
982 apply (rule lambda_abs2) |
983 apply (rule fr_lam_replace, assumption) |
|
984 apply (rule Relation1_formula_rec_case) |
983 apply (rule Relation1_formula_rec_case) |
985 apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) |
984 apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) |
986 done |
985 done |
987 |
986 |
988 lemma (in Formula_Rec) fr_transrec_closed: |
987 lemma (in Formula_Rec) fr_transrec_closed: |