Diffusion Isabelle c84a20e9b00f

correctly parse E proofs that assume '=' and '!=' bind more tightly than…
c84a20e9b00f
Actions

Tags

None

Subscribers

None

Description

correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives

Details

Provenance

Authored on

Parents

rISABELLEec18dcd6e85f: don't lose error messages

Branches

Unknown

Tags

Unknown

Event Timeline

blanchette committed rISABELLEc84a20e9b00f: correctly parse E proofs that assume '=' and '!=' bind more tightly than….Feb 1 2022, 4:16 PM

Changes (1)

Path

Size

src/

HOL/

Tools/

ATP/

rISABELLEc84a20e9b00f

src/HOL/Tools/ATP/atp_proof.ML

Loading...