doc-src/Contents

export consts_of;
removed const_expansion;
pretty_term', infer_types(_simult): separate Consts.T argument;
added generic certify;
simplified certify_term/prop;

Ref System Logics HOL ZF Inductive AxClass TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar