search

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

Proof object: ids #18

Closed windsteiger closed 11 years ago

windsteiger commented 11 years ago

Rethink assignment of ids to proof nodes: Currently, the ids are inherited from the open proof sit and need to be "renewed" (->renewID) afterwards. Why don't we immediately assign unique new ids when the node is created?

windsteiger commented 11 years ago

Fixed and simplified. When we create PRINFO, we generate a unique id immediately. renewID is then not necessary anymore, we removed renewID. The generation of the proof tree needed only minor modification.