reject_vars: accept type-inference params;
standard_term_check: include prepare_pattern;
infer_type: mode_schematic;
tuned;
Ref System Logics HOL ZF Inductive AxClass TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar IsarAdvanced/Classes IsarAdvanced/Codegen IsarAdvanced/Functions