delete attribute for code abbrev

dropped term_of obfuscation -- not really required; tuned theory structure

hardcoded nbe and sml into value command

modernized setups

degeneralized value command into HOL

dimiss simplified as evaluator due to little practical relevance

prefer separate command for approximation

removed junk from library theory

note of_class rule for type classes in theory: useful to promote class instance proofs to locale interpretation proofs

normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; tuned naming; dropped dead parameters;

tuned GUI;

clarified detach_operation: ignore empty output;

bounce focus back to main text area -- Output is for output, not query input;

update for release;

merged

tuned message;

no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;

some position markup to help locating the query context, e.g. from "Info" dockable;

tuned GUI;

tuned GUI;

tuned GUI;

tuned message: more compact, imitate actual command line;

enable "PIDE" docking framework by default, and rely on its "Detach" menu item;

some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;

untyped, unscoped, unchecked access to JVM objects;

Documented new property

generate 'map_ident' theorem for BNFs

explicit option to build library, which takes most of the time; produce minimal index, e.g. for test web page;