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;

standardized action and panel names;

tuned imports;

prefer concrete list append;

tuned whitespace;

more standard names for protocol and markup elements;

tuned whitespace;

tuned signature;

generic markup for embedded languages;

clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;

more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;

subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);

always show PIDE positions as \<here> (0x002302 "House" from DejaVuSansMono);

hyperlink for visible positions;

more informative error;

more informative error;

removed not anymore used theorems

syntactic simplifications of internal (co)datatype constructions

follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions

simplified data structure by reducing the incidence of clumsy indices

tuning * * * moved 'primrec' up to displace the few remaining uses of 'old_primrec'

made SML/NJ happy;

NEWS;

name derivations in 'primrec' for code extraction from proof terms

renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)