improved error output -- variant/mark bounds;
simplified infer_types -- always freeze, no result substitution;
Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar IsarAdvanced/Classes IsarAdvanced/Codegen IsarAdvanced/Functions