tuned signature;

tuned signature;

tuned signature -- more abstract PIDE editor operations;

tuned messages

clarified option name (since case/fold/rec are also destructors)

define case constant from other 'free constructor' axioms

introduced case tactics

tuning

handle both TVars and TFrees -- necessary for 'wrap_free_constructors'

qualify map and rel names

reverted ill-advised naming scheme of 5a77edcdbe54

made (hopefully temporary) hack more robust

added warning

gracefully handle one more error condition

gracefully fail to define polymorphic (co)datatypes in local context

made code more robust

avoid DUP exception in local context (cf. 062aa11e98e1)

honor user tfree names

prefer local facts over global ones

use local context for name space

explicit "strict" flag for print functions (flipped internal meaning); non-strict query operations may operate on failed states;

avoid unnecessary case distinction

adjust tooltip for duplicates option

merged

NEWS;

Find is docked on startup;

sorted lines;

tuned GUI;

retain current task priority, to avoid distortion due to local forks (e.g. sledgehammer query operation);

removed "Locate" button, to avoid confusion about the slightly odd meaning of current_command with explicit theory context;