more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)

new approach to silence proof methods, to avoid weird theory/context mismatches

type

merged

restrict default docking layout to bare minimum -- NB: Simplifier Trace still needs fine-tuning to show up on demand;

updated isatest;

updated to polyml-5.5.2;

practically obsolete: plain "poly" should work, except for Linux without libgmp installed;

updated to polyml-5.5.2;

document 'set_empty'

generate 'set_empty' theorem for BNFs

document 'map_id0'

note map_id0 more often

added lemma

added lemmas

transfer theorems since 'silence_methods' may change the theory

add mono rules for diff

clean up Lebesgue integration

more bnf_decl -> bnf_axiomatization

tuned docs

hide more internal names

tuning

no reset for 'end' -- e.g. relevant for 'notepad';

updated keywords

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;

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;