Diffusion Isabelle 73b120e0dbfe

generate some metainformation not only for SPASS but also for Zipperposition…
73b120e0dbfe
Actions

Tags

None

Subscribers

None

Description

generate some metainformation not only for SPASS but also for Zipperposition, for experimentation

Details

Provenance

Authored on

Parents

rISABELLE5836811fe549: added lemma wfP_subset_mset[simp]

Branches

Unknown

Tags

Unknown

Event Timeline

blanchette committed rISABELLE73b120e0dbfe: generate some metainformation not only for SPASS but also for Zipperposition….Oct 17 2022, 1:04 PM

Changes (4)

Path

Size

src/

HOL/

Tools/

ATP/

atp_problem_generate.ML

Sledgehammer/

sledgehammer_atp_systems.ML

sledgehammer_prover_atp.ML

rISABELLE73b120e0dbfe

src/HOL/Tools/ATP/atp_problem.ML

Loading...

src/HOL/Tools/ATP/atp_problem_generate.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

Loading...