Diffusion Isabelle 75f5c63f6cfa

better handling of skolemization for Isar reconstruction in Sledgehammer for…
75f5c63f6cfa
Actions

Tags

None

Subscribers

None

Description

better handling of skolemization for Isar reconstruction in Sledgehammer for veriT

Details

Provenance

Authored on

Parents

rISABELLE83b5911c0164: more lemmas

Branches

Unknown

Tags

Unknown

Event Timeline

Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> committed rISABELLE75f5c63f6cfa: better handling of skolemization for Isar reconstruction in Sledgehammer for….Oct 28 2020, 8:41 AM

Changes (7)

Path

Size

src/

HOL/

SMT_Examples/

SMT_Tests_Verit.thy

Tools/

SMT/

smt_replay_arith.ML

verit_replay.ML

verit_replay_methods.ML

Sledgehammer/

sledgehammer_isar.ML

rISABELLE75f5c63f6cfa

src/HOL/SMT.thy

Loading...

src/HOL/SMT_Examples/SMT_Tests_Verit.thy

Loading...

src/HOL/Tools/SMT/smt_replay_arith.ML

Loading...

src/HOL/Tools/SMT/verit_proof.ML

Loading...

src/HOL/Tools/SMT/verit_replay.ML

Loading...

src/HOL/Tools/SMT/verit_replay_methods.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

Loading...