Change.Snapshot: include from_current/to_current here, with precomputed changes;

explicit Change.Snapshot and Document.Node; misc tuning and clarification; Document_View: explicitly highlight outdated command status;

simplified/refined document model: collection of named nodes, without proper dependencies yet; moved basic type definitions for ids and edits from Isar_Document to Document; removed begin_document/end_document for now -- nodes emerge via edits; edits refer to named nodes explicitly;

somewhat uniform Thy_Header.split_thy_path in ML and Scala;

uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);

load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;

export use_thys_wrt;

more precise CRITICAL sections, using NAMED_CRITICAL uniformly;

updated to Netbeans 6.9;

schedule_futures: discontinued special treatment of non-parallel proofs, which might have affected memory usage at some point, but does not seem to make a difference with as little as 2GB RAM;

more precise CRITICAL sections; tuned;

removed unused Update_Time data (cf. ac94ff28e9e1);

modernized specifications; tuned headers;

eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;

find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);

renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);

tuned headers -- more precise load path;

theory loading: only the master source file is looked-up in the implicit load path;

load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;

simplified/clarified Thy_Load path: search for master only, lookup other files relative to that; tuned;

only test prolog code examples if environment variable is set

Revised proof of long division contributed by Jesus Aransay.

fix bug with Kodkodi < 1.2.14

merged

document new Nitpick options

tweak datatype sym break code

added manual symmetry breaking for datatypes

change the order of the SAT solvers, from fastest to slowest

started implementation of custom sym break

clarify Nitpick's output in case of a potential counterexample

added support for CryptoMiniSat

gracefully handle the case where no integers occur in the formula and the "max" option is used

merged

adding Code_Prolog theory to IsaMakefile and HOL-Library root file

inductive_simps learns to have more tool compliance

setting up Code_Prolog_Examples

adding queens and symbolic derivation example for prolog code generation

adding parsing of numbers; improving output of solution without free variables in prolog code generation

adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation

adding basic arithmetic support for prolog code generation

adding numbers as basic term in prolog code generation

More consistent naming of locale api functions.

Documentation of 'interpret' updated.

print_interps shows interpretations in proofs.

Interpretation in proofs supports mixins.

Make registrations generic data.

merged

don't choke on synonyms when parsing SPASS's Flotter output + renamings; the output format isn't documented so it was hard to guess that a single clause could be associated with several names...

fix Mirabelle timeout

make Mirabelle happy

fix bug in the newly introduced "bound concealing" code

handle division by zero gracefully (used to raise Unordered later on)

use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures; this replaces the previous, somewhat messy solution of adding "extra" clauses

fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)

handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs

revert exception throwing in FOL_SOLVE, since they're not caught anyway

avoid "ATP Error: Error: blah" style messages

avoid "_def_raw" theorems

better error and minimizer output

deal with chained facts more gracefully