support embedded syntax, for use with control symbols;

tuned;

tuned;

clarified default: final value is provided in Isabelle/Scala Latex.Cite.unapply;

more "cite" antiquotations;

clarified signature: more generic operations;

avoid confusion of markup element vs. property names;

clarified check: this could be \nocite;

clarified Latex markup: optional cite "location" consists of nested document…

more explicit latex markup;

follow recent changes of Sledgehammer defaults, as 0a46b3dbd5ad exposes a hint…

One messy, messy proof

Missing theorem restored

Tidying up BNF

More cleaning up proofs, plus a TeX fix

Fixed a broken proof

Substantial simplification of HOL-Cardinals

merged

Trying to clean up HOL/Cardinals

Removed a reference to the (redundant) wf_restr

added bibliographies to ROOTs;

added session to mirabelle output directory structure

More tidying of topology proofs

Partial round of clearing up applys, etc

merged

Substantial de-applying and streamlining

merged

tuned sledgehammer default provers to only include local ones

Changes for generalised lemmas

Changes for generalised lemmas

Generalised Lemmas

enforce rebuild of Isabelle/ML to update build databases;

prefer relative src_path (if possible) -- in contrast to 9ce0aa145d21:

proper treatment of unicode_symbols;

tuned signature: avoid alias that is unclear wrt. lazy state and Symbol.

removed unused operation: unclear wrt. Symbol.encode/decode status;

tuned signature: more uniform operations;

tuned comments;

restrict to proper_session_theories;

more uniform operations;

unused;

proper build parameters (amending d858e6f15da3);

treat update_options as part of Sessions.Info meta_digest, for proper re-build…

more command-line options;

tuned options --- avoid confusion with "isabelle build -b";

tuned signature;

isabelle update -u path_cartouches;

updated documentation;

merged

more options;

tuned message;

isabelle update no longer uses PIDE dump, but regular session build database…

proper Node.init_blobs, not just edits (amending ca872f20cf5b);

more robust;

more operations;

clarified session sources: theory and blobs are read from database, instead of…

tuned signature;

tuned;

tuned signature;

clarified signature: more operations;

clarified signature: more operations;

tuned;

more direct access to session_sources, without somewhat fragile file-system…

tuned;

tuned signature;

tuned signature: avoid confusion with Document.Node.Blob and Command.Blob;

clarified signature: old node is ignored;

clarified signature;

tuned;

final tidying of theorems

merged

merged

continued proof simplification

Further simplifications

More tidying of proofs

merged

tuned;

merged

discontinued fragile operation;

more robust operations: avoid somewhat fragile Document.Node.Name.

tuned;

tuned whitespace;

avoid somewhat fragile Document.Node.Name.master_dir_path;

tuned;

clarified signature: avoid somewhat fragile Document.Node.Name.master_dir_path;

tuned;

clarified modules;

tuned;

clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;

clarified modules;

tuned signature: avoid too many aliases (see also 72daee8a39ca);

merged

strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and…

merged

adapted to Isabelle/c9e091867206

tuned;

Fixed a couple of simple_path occurrences

merged

Tidying up of paths, introducing "loop_free" as a separate predicate in the…

clarified signature: more explicit types;