HomeIsabelle/Phabricator

use simplifier to classify the missing assumptions in Sledgehammer's abduction…