Initial proof object: use previously generated object

windsteiger / Theorema

Theorema: A System for Automated Reasoning (Theorem Proving) and Automated Theory Exploration based on Mathematica

GNU General Public License v3.0

70 stars 14 forks source link

Initial proof object: use previously generated object #21

Open windsteiger opened 11 years ago

windsteiger commented 11 years ago

Offer the possibility to continue on a previously generated proof object. InitialProofObject not an empty one, but one available from a prior run. (Raised by tkutsia seminar January 9, 2013)

windsteiger commented 11 years ago

Make SearchDepth a local value in a proof node -> different branches could get different depths when continuing a proof.