* Sledgehammer no longer produces structured proofs by default. To enable, declare [[sledgehammer_full = true]]. Attributes reconstruction_modulus, reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts. INCOMPATIBILITY. Larry