Diffusion Isabelle c7e2a9bdc585

Added support for TFX to Sledgehammer
c7e2a9bdc585
Actions

Tags

None

Subscribers

None

Description

Added support for TFX to Sledgehammer

Details

Provenance

Authored on

Parents

rISABELLE18eb7ec2720f: Tuned indentation

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rISABELLEc7e2a9bdc585: Added support for TFX to Sledgehammer.Nov 5 2020, 6:14 PM

desharna mentioned this in rISABELLE5f7d86b28ffb: repaired thf output broken by c7e2a9bdc585.Nov 19 2020, 4:21 PM

desharna mentioned this in rISABELLEf8d25850173b: reintroduced and renamed THF_Predicate_Free deleted by c7e2a9bdc585.

Changes (12)

Path

Size

Sledgehammer.thy

atp_problem_generate.ML

Sledgehammer/

sledgehammer_atp_systems.ML

rISABELLEc7e2a9bdc585

src/HOL/ATP.thy

Loading...

src/HOL/Sledgehammer.thy

Loading...

src/HOL/Tools/ATP/atp_problem.ML

Loading...

src/HOL/Tools/ATP/atp_problem_generate.ML

Loading...

src/HOL/Tools/ATP/atp_proof.ML

Loading...

src/HOL/Tools/ATP/scripts/dummy_atp

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML

Loading...