always show PIDE positions as \<here> (0x002302 "House" from DejaVuSansMono);

hyperlink for visible positions;

more informative error;

more informative error;

removed not anymore used theorems

syntactic simplifications of internal (co)datatype constructions

follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions

simplified data structure by reducing the incidence of clumsy indices

tuning * * * moved 'primrec' up to displace the few remaining uses of 'old_primrec'

made SML/NJ happy;

NEWS;

name derivations in 'primrec' for code extraction from proof terms

renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)

updated NEWS

updated keywords

renamed 'datatype_new_compat' to 'datatype_compat'

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