dropped long-unused option

avoid ad-hoc patching of generated code

tuned proofs;

support for semantic completion on Scala side;

clarified module location (again, see 763d35697338);

support for completion within the formal context; tuned signature;

removed remains of old experiment (see b933142e02d0);

removed dead code; more complete patterns;

tuned signature;

NEWS;

tuned comment;

refined language context: antiquotes; support default completions, with move of caret position; tuned signature;

tuned proofs;

merged

more standard theory name;

tuned;

tuned whitespace; tuned names;

proper ML structure with signature;

reduced ML warnings;

simultaneous mapping of strongly connected components

dropped dead code

more symbols;

merged

improved completion based on context information;

more markup -- complete symbols within antiquotation, notably with broken arguments;

eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);

tuned signature -- avoid redundancy and confusion of flags;

tuned signature;

more general / abstract Command.Markups, with separate index for status elements; slightly faster Rendering.overview_color;

tuned signature -- avoid obscure default arguments;

more lightweight Rendering;

tuned signature;

tuned -- remaining rev_markup is rather short after filter;

only one internal coinduction rule

NEWS

adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package

tuned proofs; more symbols;

tuned whitespace;

updated keywords;

merged

more official params in context;

tuned signature; tuned message;

tuned messages; more official hyps;

clarified printing of undeclared hyps;

modernized tool setup; tuned;

removed dead code;

tuned;

proper naming convention;

prefer cat_lines;

tuned whitespace;

tuned comments;

complete symbols within ML strings / comments;

tuned messages;

tuned;

clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;

added PIDE.snapshot, PIDE.rendering for convenience;

cumulate/select wrt. precise elements guard; tuned signature;

tuned;

tuned imports;

unused;

default completion context via outer syntax; no symbol completion for ML files; tuned;

completion of keywords and symbols based on language context;

prefer guarded Context_Position.report where feasible;

more markup; clarified token range;

tuned signature;

removed dead code;

refactoring; generate rep_eq always, not only when it would be accepted by the code generator

refactoring

the rule is not needed due to 1726f46d2aa8

merged

tuned tactic

tuned

less flex-flex pairs

less flex-flex pairs (thanks to Lars' statistics)

made tactics more robust

offical tool

more convenient syntax for permanent interpretation

aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"

move stronger rules into exercise

added a function that carries out all the reconstruction steps, for improved usability; added documentation;

reconstruction framework for LEO-II's TPTP proofs;

made list of test files a parameter to timed_test in TPTP_Test.thy, and updated dependent definitions;

cleaned code used to produce a proof-graph;

improved configurability of DOT exporter; tuned;

behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not; tuned;

experimented with presentation of DOT+LaTeX;

edges are now being shown in the proof graph; removed the shapes related to the conjecture and the negated conjecture, to remove clutter (since i'm also showing the inference's conclusion in latex);

added case for handling 'assumption' lines in Satallax proofs;

improved latex output: spacing between terms, and encoding terms in mathrm; tuned comments;

experimenting with improving DOT output, and embedding LaTeX code for formulas (rather than only giving the clause number);

added more node shapes (matched with roles);

updated NEWS

merged 'List.set' with BNF-generated 'set'

moved advanced folding into separate exercise

tuned definition

another simplification of internal codatatype construction

reflect 207538943038 in NEWS

reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes

removed not anymore used constants and theorems

simplifications of internal codatatype construction

adapted Nitpick to 'primrec' refactoring

moved 'primrec' up (for real this time) and removed temporary 'old_primrec'

rewrote a small portion of code to avoid dependency on low-level constant

tuning

provide more automation for type definitions (makes book exercises easier)

prepare two-stage 'primrec' setup

tuning

removed deadcode

merged

tuning

made SML/NJ happier

simplify proofs because of the stronger reflexivity prover

delete or move now not necessary reflexivity rules due to 1726f46d2aa8

implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules

merged

more markup;

proper term equality; proper Args.term_pattern parser (like 'is' or 'let' in Isar);

tuned message;

more uniform treatment of dockables and their standard actions;