An object logic's syntax and inference rules are specified

declaratively allowing single-step proof construction.

Proof procedures can be expressed using "tactics" and

"tacticals". Isabelle provides control structures for

expressing search procedures and generic tools such as

simplifiers and classical theorem provers which can be applied

to object-logics. Isabelle is built on top of Standard ML

and uses its user interface.