HomeIsabelle/Phabricator
Diffusion Isabelle bc43f86c9598

added refute mode to Sledgehammer to find 'counterexamples'
bc43f86c9598
Actions

Description

added refute mode to Sledgehammer to find 'counterexamples'

Details

Provenance
blanchetteAuthored on
Parents
rISABELLE9653bea4aa83: merged
Branches
Unknown
Tags
Unknown

Changes (14)

PathSize
src/
Doc/
Sledgehammer/
document/
HOL/
Tools/
SMT/
Sledgehammer/

rISABELLEbc43f86c9598

View Options

NEWS

Loading...
View Options

src/Doc/Sledgehammer/document/root.tex

Loading...
View Options

src/HOL/Tools/SMT/smt_solver.ML

Loading...
View Options

src/HOL/Tools/SMT/smt_systems.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_fact.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...