Add 'empty?' spec.

Replace redundant association by method The goals array was never set when proving and it can be retrieved through the ProofAttempts anyway.

Remove locid from ProofAttemptConfiguration This is not needed anymore because we have a one-to-one relation between ProofAttemptConfiguration and ProofAttempt.

Let PAC have one proof_attempt and remove goals When the ProofAttemptCofiguration only has one proof_attempt, there can only be a single goal. This can be retrieved through the proof_attempt.

Adjust specs to new AxiomSelection.

Add locid and number to ProofAttemptConfiguration.

Add model: ProofAttemptConfiguration.