Diffusion Isabelle 9231ea46e041

promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
9231ea46e041
Actions

Tags

None

Subscribers

None

Description

promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"

Details

Provenance

Authored on

Parents

rISABELLEd593d18a7a92: merged

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rISABELLE9231ea46e041: promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules".Jul 8 2021, 3:25 PM

Changes (7)

Path

Size

src/

HOL/

Tools/

Sledgehammer/

sledgehammer.ML

sledgehammer_commands.ML

sledgehammer_fact.ML

sledgehammer_mash.ML

sledgehammer_prover.ML

sledgehammer_prover_minimize.ML

sledgehammer_tactics.ML

rISABELLE9231ea46e041

src/HOL/Tools/Sledgehammer/sledgehammer.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML

Loading...