Diffusion Isabelle 18cd39e55eca

have Sledgehammer honor 'smt_nat_as_int' option
18cd39e55eca
Actions

Tags

None

Subscribers

None

Description

have Sledgehammer honor 'smt_nat_as_int' option

Details

Provenance

Authored on

Parents

rISABELLEf12539c8de0c: more handling of Zipperposition definitions in Isar proof construction

Branches

Unknown

Tags

Unknown

Event Timeline

blanchette committed rISABELLE18cd39e55eca: have Sledgehammer honor 'smt_nat_as_int' option.Feb 22 2022, 3:00 PM

Changes (2)

Path

Size

src/

HOL/

Tools/

ATP/

Sledgehammer/

sledgehammer_prover_smt.ML

rISABELLE18cd39e55eca

src/HOL/Tools/ATP/atp_util.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML

Loading...