HomeIsabelle/Phabricator
Diffusion Isabelle b087610592b4

rationalized output for forthcoming slicing model
b087610592b4
Actions

Description

rationalized output for forthcoming slicing model

Details

Provenance
blanchetteAuthored on
Parents
rISABELLE30a619de7973: use same default for FO and HO provers w.r.t. induction principles, based on…
Branches
Unknown
Tags
Unknown

Changes (7)

PathSize
src/
HOL/
Tools/
Sledgehammer/

rISABELLEb087610592b4

View Options

src/HOL/Tools/Sledgehammer/sledgehammer.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML

Loading...