merged

Tidied some messy old proofs

merged

more markup for syntax consts;

more markup for syntax consts;

clarified concrete syntax;

more accurate markup (amending 43c4817375bf): only consider primitive syntax consts, avoid extra Markup.intensify e.g. due to "\<^const>Pure.all_binder";

more concrete syntax and more checks;

clarified signature: more operations;

support for syntax const dependencies, with minimal integrity checks;

tuned;

clarified markup: more uniform treatment of parse/print phase;

tuned;

clarified markup: more uniform;

tuned signature: separate markup vs. extern;

clarified signature;

tuned: prefer configuration options via context;

tuned;

tuned signature: more operations;

tuned comments

merged

Partial tidying of old proofs

merged

new version of time_fun that works for classes; define T_length automatically now

merged

revised/generalised some lemmas

remove terminated jobs, even if futures do not complete;

terminate jobs properly;

clarified signature: eliminate clones;

tuned: more antiquotations;

tuned: more antiquotations;

misc tuning;

tuned: eliminate clone (with change of internal exceptions);

tuned: more antiquotations;

tuned comments and whitespace (see also 589645894305);

tuned: more antiquotations;

tuned: more antiquotations;

proper const (see also 759bffe1d416 and b2800da9eb8a);

tuned: inline constants;

tuned: eliminate clone;

tuned: more antiquotations;

prefer host that is less likely to be down;

adapt and activate congprocs examples, following the current Simplifier implementation; minor tuning;

original Congproc_Ex.thy by Norbert Schirmer: still inactive;

provide Simplifier.set_mksimps_context (roughly following Norbert Schirmer): allow update of context when premises are added to the local simpset;

clarified signature;

more direct access to Simplifier.mk_cong, to avoid odd Simpdata.mk_meta_cong seen in the wild;

tuned;

support for congprocs in the Simplifier, closely following Norbert Schirmer et-al, but with only one "simproc" name space and "simproc_setup" command / ML antiquotation;

tuned;

tuned: anticipate congprocs;

clarified signature;

tuned signature (again): anticipate different kinds of procs;

clarified context data; tuned: more antiquotations;

tuned: prefer canonical argument order;

tuned: more antiquotations;

tuned: prefer canonical argument order;

clarified signature: less redundant types;

clarified signature;

unused (see d12c58e12c51);

tuned signature: support more general procedures;

merged

tuned: more antiquotations;

tuned;

tuned: more antiquotations;

tuned whitespace;

more robust (amending 8f53fa93d5f0): R could be anything and Thm.instantiate' involves some type-checks, e.g. relevant for lemma fset_simps in theory Quotient_Examples.Quotient_FSet;

tuned modules;

misc tuning;

tuned;

tuned: more antiquotations;

misc tuning;

misc tuning and clarification;

tuned;

misc tuning and clarification: proper context, proper exception;

tuned: eliminate odd clones;

tuned: more antiquotations;

unused;

tuned: more antiquotations;

tuned: more antiquotations;

tuned: more antiquotations;

tuned proofs;

tuned signature: more operations;

tuned;

tuned: more antiquotations;

clarified signature;

Two little lemmas

merged

more uniform Type_Infer_Context.infer_types_finished, despite subtle differences of Type_Infer.fixate vs. Proof_Context.standard_term_check_finish;

tuned, following cdae621613da;

tuned;

more robust: only type inference with its finish/fixate phase (on contrast to dc387e3999ec), e.g. avoid accidental "improvement" of type class operations (free vs. const);

tuned: more antiquotations;

tuned: more abstract access to datatype typ;

tuned (see also db120661dded);

tuned: more antiquotations;