equal
deleted
inserted
replaced
450 |
450 |
451 |
451 |
452 (* close_derivation *) |
452 (* close_derivation *) |
453 |
453 |
454 fun close_derivation thm = |
454 fun close_derivation thm = |
455 if Thm.derivation_name thm = "" then Thm.name_derivation "" thm |
455 if Thm.derivation_closed thm then thm else Thm.name_derivation "" thm; |
456 else thm; |
|
457 |
456 |
458 |
457 |
459 (* user renaming of parameters in a subgoal *) |
458 (* user renaming of parameters in a subgoal *) |
460 |
459 |
461 (*The names, if distinct, are used for the innermost parameters of subgoal i; |
460 (*The names, if distinct, are used for the innermost parameters of subgoal i; |