equal
deleted
inserted
replaced
1092 in |
1092 in |
1093 EVERY' [lambda_prs_tac lthy quot, |
1093 EVERY' [lambda_prs_tac lthy quot, |
1094 TRY o simp_tac simp_ctxt, |
1094 TRY o simp_tac simp_ctxt, |
1095 TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1095 TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1096 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), |
1096 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), |
1097 rtac refl] |
1097 TRY o rtac refl] |
1098 end |
1098 end |
1099 *} |
1099 *} |
1100 |
1100 |
1101 section {* Genralisation of free variables in a goal *} |
1101 section {* Genralisation of free variables in a goal *} |
1102 |
1102 |