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