Overview

A set of Isabelle proof methods and commands that facilitates the use of relatively complete decision procedures (e.g. SMT solvers and paramodulation-based provers) with deterministic quantifier instantiation based on bounded E-matching. More about TSMT is explained in the TSMT Tutorial.