bnf_decl -> bnf_axiomatization

tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";

Replaced refute with nitpick.

NEWS;

tuned message;

smarter recovery from toplevel type error;

more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion; prefer JDialog for FloatingWindowContainer, to keep it in front of the main window; updated to Navigator.jar 2.5, SideKick.jar 1.6;

updated keywords;

merged

more markup;

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

always bounce focus back to main text area, unless explicit focus component is given here (see also 7b65f4da136d);

tuned signature;

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;