equal
deleted
inserted
replaced
363 *) |
363 *) |
364 in |
364 in |
365 (* ~j because new asm starts at back, thus we subtract 1 *) |
365 (* ~j because new asm starts at back, thus we subtract 1 *) |
366 Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i)) |
366 Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i)) |
367 (Tactic.dtac preelimrule i th2) |
367 (Tactic.dtac preelimrule i th2) |
368 |
|
369 (* (Thm.bicompose |
|
370 false (* use unification *) |
|
371 (true, (* elim resolution *) |
|
372 elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems) |
|
373 i th2) *) |
|
374 end; |
368 end; |
375 |
369 |
376 |
370 |
377 (* prepare to substitute within the j'th premise of subgoal i of gth, |
371 (* prepare to substitute within the j'th premise of subgoal i of gth, |
378 using a meta-level equation. Note that we assume rule has var indicies |
372 using a meta-level equation. Note that we assume rule has var indicies |