document idiomatic use of 'simps_of_case'

ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction

register old-style datatypes as 'Ctr_Sugar'

export useful ML function

moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it

tuned headers

moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction

updated sessions;

proper latex -- NB: cannot use antiquotation here;

merged

simplified App template;

obsolete;

obsolete;

tuned message;

tuned signature -- removed obsolete Addsimprocs, Delsimprocs;

tuned signature;

minor doc fix

merged

merged, using src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML and src/HOL/Tools/Sledgehammer/sledgehammer_run.ML from 347c3b0cab44;

removed obsolete RC tags;

Added tag Isabelle2013-1 for changeset 9c1f21365326

tuned;

more on completion;

adjust modules for Admin/build jars_test;

tuned whitespace;

added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);

transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;

Added tag Isabelle2013-1-RC4 for changeset 594628261376

updated to polyml-5.5.1-1 (fixes-5.5.1 version 1875);

tuned;