Changes

Summary

removed rarely used error in Sledgehammer
merged
tuned
added refute mode to Sledgehammer to find 'counterexamples'

Changeset 77272:0506c3273814 by blanchet: removed rarely used error in Sledgehammer
The file was modified	`src/HOL/Tools/ATP/atp_proof.ML` (diff)
The file was modified	`src/HOL/Tools/ATP/atp_proof_reconstruct.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML` (diff)
Changeset 77271:40b23105a322 by nipkow: merged
Changeset 77270:d1ca1e587a8e by nipkow: tuned
The file was modified	`src/HOL/Data_Structures/RBT_Map.thy` (diff)
Changeset 77269:bc43f86c9598 by blanchet: added refute mode to Sledgehammer to find 'counterexamples'
The file was modified	`NEWS` (diff)
The file was modified	`src/Doc/Sledgehammer/document/root.tex` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_solver.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_systems.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML` (diff)
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML` (diff)