Diffusion Isabelle 0fa4bebbdd75

support Zipperposition's skolemization in generated Isar proofs
0fa4bebbdd75
Actions

Tags

None

Subscribers

None

Description

support Zipperposition's skolemization in generated Isar proofs

Details

Provenance

Authored on

Parents

rISABELLE3e30ca77ccfe: improved output in simps_case_conv;

Branches

Unknown

Tags

Unknown

Event Timeline

blanchette committed rISABELLE0fa4bebbdd75: support Zipperposition's skolemization in generated Isar proofs.Feb 27 2024, 2:08 PM

Changes (3)

Path

Size

src/

HOL/

Tools/

ATP/

atp_proof_reconstruct.ML

Sledgehammer/

sledgehammer_prover_atp.ML

rISABELLE0fa4bebbdd75

src/HOL/Tools/ATP/atp_proof.ML

Loading...

src/HOL/Tools/ATP/atp_proof_reconstruct.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

Loading...