Diffusion Isabelle ef89f1beee95

parse applie lambdas correctly plus deal gracefully with lambda-lifting in…
ef89f1beee95
Actions

Tags

None

Subscribers

None

Description

parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition

Details

Provenance

Authored on

Parents

rISABELLE41273636a82a: added argo

Branches

Unknown

Tags

Unknown

Event Timeline

blanchette committed rISABELLEef89f1beee95: parse applie lambdas correctly plus deal gracefully with lambda-lifting in….Sep 25 2023, 5:16 PM

Changes (4)

Path

Size

src/

HOL/

Tools/

ATP/

atp_proof_reconstruct.ML

Sledgehammer/

sledgehammer_isar.ML

sledgehammer_isar_proof.ML

rISABELLEef89f1beee95

src/HOL/Tools/ATP/atp_proof.ML

Loading...

src/HOL/Tools/ATP/atp_proof_reconstruct.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML

Loading...