renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)

tuning: moved code where it belongs

have 'primrec_new' fall back on old 'primrec' when given old-style datatypes

tuning

more markup;

folded 'rel_option' into 'option_rel'

folded 'list_all2' with the relator generated by 'datatype_new'

removed final periods in messages for proof methods

tuned proofs;

added a version of the Metis tactic that returns the unused facts

tuned code

more NEWS

folded 'Option.set' into BNF-generated 'set_option'

merged

prefer user-space tool within Pure.thy;

more markup;

more uniform rendering of text that is formally interpreted: avoid clash with inner markup;

recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;

support ML antiquotations in Scala; tuned -- more uniform ML vs. Scala;

antiquotations within plain text: Scala version in accordance to ML;

tuned signature -- emphasize line-oriented aspect;

eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)

tuned whitespace;

removed odd comments -- inferred types are shown by Prover IDE;

removed dead code; tuned;

more uniform ML keyword markup; tuned;

merged

tuned;

clarified Isabelle/ML strings;

refined ML keyword styles;