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);