Diffusion Isabelle 51dac6fcdd0e

reverted 0506c3273814 -- the message is still useful
51dac6fcdd0e
Actions

Tags

None

Subscribers

None

Description

reverted 0506c3273814 -- the message is still useful

Details

Provenance

Authored on

Parents

rISABELLE110988ad5b4c: compile

Branches

Unknown

Tags

Unknown

Reverts

rISABELLE0506c3273814: removed rarely used error in Sledgehammer

Event Timeline

blanchette committed rISABELLE51dac6fcdd0e: reverted 0506c3273814 -- the message is still useful.Mar 1 2023, 8:00 AM

blanchette added a reverted change: rISABELLE0506c3273814: removed rarely used error in Sledgehammer.Mar 1 2023, 5:27 PM

Changes (4)

Path

Size

src/

HOL/

Tools/

ATP/

atp_proof_reconstruct.ML

Sledgehammer/

sledgehammer_prover_atp.ML

rISABELLE51dac6fcdd0e

src/HOL/Tools/ATP/atp_proof.ML

Loading...

src/HOL/Tools/ATP/atp_proof_reconstruct.ML

Loading...

src/HOL/Tools/ATP/atp_util.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

Loading...