tuned;

discontinued mostly unused markup for command spans;

more visible markup of malformed input as "bad";

tuned proofs

some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;

refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.; tuned signature;

tuned signature;

more direct Linear_Set.reverse, swapping orientation of the graph; tuned;

tuned signature;

tuned;

refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;

explicit FIXME;

tuned signature;

corrected header

refined isabelle mkroot; allow empty 'theories' to facilitate generated templates;

simplified session specifications: names are taken verbatim and current directory is default;

added build option -D: include session directory and select its sessions;

discontinued obsolete "isabelle makeall";

even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);

back to implicit commit via isabelle-process -- save image only once (cf. 181b91e1d1c1);

proper axiomatization of "mem" -- do not leave it formally unspecified;

simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;

more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;

obsolete;

eliminated obsolete ISABELLE_USEDIR_OPTIONS;

updated ML settings;

add legacy target for HOL-Probability, needed by AFP/Markov_Models

proper isabelle update_keywords tool;

configure Admin as component, with its own lib/Tools;

SOMEthing went utterly wrong in 5b51ccdc8623;

more legacy targets;

discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;

tuned;

proper quoting

merged

more structural parsing for minor modes; tuned signatures;

clarified Sidekick configuration, including minor modes;

stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users

specify full path to clausifier

documentation

more token markers, based on actual outer syntax; prefer official Outer_Syntax.init with its completions;

simplified process startup phases: INIT suffices for is_ready;

need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";

prefer static Build.session_content for loaded theories -- discontinued incremental protocol;

prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol; just one cumulative Keyword.status at end of batch session;

permissive outer syntax wrt. symbol recoding;

simplified Document.Node.Header -- internalized errors;

tuned signature;

tuned signature -- slightly more abstract text representation of prover process;

tuned signature -- make Pretty less dependent on Symbol;

extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)

increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)

documentation

added iProver(-Eq) local

optimized saving

pass Isabelle/Scala system options into ML process of Isar tty or build jobs;

merged

switching from Emacs.app to Aquamacs.app

switching from Emacs.app to Aquamacs.app

modify group_cancel simprocs so that they can cancel multiple terms at once

"isabelle options" prints Isabelle system options;

removed leftover from 89cc3dfb383b, hoping that mira digests it;

discontinued presumably obsolete attempts at doc-src testing (cf. 3b02b0ef8d48, 89cc3dfb383b);

more precise imitation of old ROOT.ML files;

fixed mira.py (cf. fe611991427a)

corrected session name

removed obsolete mira configurations -- covered by AFP_images

modernized mira configurations, making use of isabelle build

removed mira configurations related to old importer

re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;

more on isabelle mkroot;

added mkroot: prepare session root directory;

prefer general Command_Line.tool wrapper (cf. Scala version);

simplified Session_Tree; tuned messages;

some timeouts, which modify the build order;

queue ordering by descending outdegree and timeout;

tuned import;

clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);

clarified Session_Entry vs. Session_Info with related parsing operations; more error positions;

simplified class Job; tuned message;

let with_timing report overall number of threads;

further robustification of interrupts during build;

refined outer syntax;

prefer calligrapic \<RR> \<II> over \<Re> \<Im> for "screen" display (NB: official unicode defines only one version of these glyphs, unlike TeX);

remember ATP flops to avoid repeating them too quickly

remember which MaSh proofs were found using ATPs

rule out same "technical" theories for MePo as for MaSh

don't generate queries for empty dependencies

crank up max number of dependencies

never use MaSh in Metis examples, to avoid one dimension of nondeterminism

merged

more informative process exit code;

timeout for session build job; tuned error messages;

static outer syntax based on session specifications;

declare trE and tr_induct as default cases and induct rules for type tr

reject path variable nesting explicitly;

simplified custom document/build script, instead of old-style document/IsaMakefile;

cleaner temporary file cleanup for MaSh, based on tried-and-trusted code

merged

don't tag negatively naked variables

support older versions of Vampire

document E-MaLeS

added E-MaLeS to list of provers for testing

discontinued unused etc/sessions catalog;

allow session specifications in arbitrary order;

tuned;

report commands as formal entities, with def/ref positions;

more official command specifications, including source position;

more antiquotations;

declare keywords only once;

more antiquotations;

more antiquotations;

more standard bootstrapping of Pure outer syntax;

fixed document;

store parent heap stamp as well -- needs to be propagated through the build hierarchy; misc tuning;

more standard bootstrapping of Pure.thy;

more precise guide for bibtex/makeindex -- dummy files should be sufficient;

added offline test for skip_proofs;

clarified ISABELLE_FULL_TEST;

explicit option skip_proofs;