equal
deleted
inserted
replaced
1375 else Seq.empty) |
1375 else Seq.empty) |
1376 (addprfs rest (n + 1)))) |
1376 (addprfs rest (n + 1)))) |
1377 in addprfs asms 1 end; |
1377 in addprfs asms 1 end; |
1378 |
1378 |
1379 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. |
1379 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. |
1380 Checks if Bi's conclusion is alpha-convertible to one of its assumptions*) |
1380 Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*) |
1381 fun eq_assumption i state = |
1381 fun eq_assumption i state = |
1382 let |
1382 let |
1383 val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; |
1383 val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state; |
1384 val (tpairs, Bs, Bi, C) = dest_state (state, i); |
1384 val (tpairs, Bs, Bi, C) = dest_state (state, i); |
1385 val (_, asms, concl) = Logic.assum_problems (~1, Bi); |
1385 val (_, asms, concl) = Logic.assum_problems (~1, Bi); |