removed debug messages; exported to_pred in InductiveSet; added further display function; adjusted mode analysis

basic support for components (which imitate the usual Isabelle directory layout);

Tuned.

the derived induction principles can be given an explicit name

updated Variable.import;

merged

merged

modernized generated example session;

added Mirabelle

Quickcheck callable from ML

future scheduler: uninterruptible cancelation;

renamed Multithreading.regular_interrupts to Multithreading.public_interrupts; renamed Multithreading.restricted_interrupts to Multithreading.private_interrupts; added Multithreading.sync_interrupts; Multithreading.sync_wait: more careful treatment of attributes; Multithreading.tracing: uninterruptible; Multithreading.system_out: signal within critical region, more careful sync_wait; eliminated redundant Thread.testInterrupt; Future.wait_timeout: uniform Multithreading.sync_wait; future scheduler: interruptible body (sync!), to improve reactivity; future_job: reject duplicate assignments -- system error; misc tuning;

recovered polyml-5.2 -- need to reload ML-Systems/multithreading.ML after overriding Thread structures;

tuned tracing;

ISABELLE_USEDIR_OPTIONS: -q 2 by default;

merged

merged

merged

cleaned up abstract tuple operations and named them consistently

cleaned up abstract tuple operations and named them consistently

added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;

trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;

retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);

qualified Subgoal.FOCUS;

FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;

focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed; added FOCUS_PREMS, which may serve as full replacement for OldGoals.METAHYPS;

Variable.importT/import: return full instantiations, tuned;

added certify_inst, certify_instantiate;

merged

trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);

proper Jinja-Slicing;

merged

merged

abstractions: desymbolize name hint

added numeral code postprocessor rules on type int

sos comments modified

sos documentation

Added remote-SOS changes by Philipp Meyer

Functionality for sum of squares to call a remote csdp prover

merged

updated generated document

reinserted legacy ML function

Set.UNIV and Set.empty are mere abbreviations for top and bot

explicit is better than implicit

Meson.first_order_resolve: avoid handle _; proper context for various Meson and Metis rules and tactics unified meson_tac/meson_claset_tac;

removed old global get_claset/map_claset; added local get_claset/put_claset;

eliminated METAHYPS;

Future.shutdown before loading sequentially -- workaround scheduler deadlock;

ResAxioms.neg_conjecture_clauses: proper context; let exceptions get through unhindered -- Poly/ML exception_trace will do the tracing;

neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS; external_prover: neg_conjecture_clauses should handle TVars within goals; misc tuning;

Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);

eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;

non-critical use_thy;

future result: Synchronized.var;

added unsynchronized Synchronized.peek;

group status: Synchronized.var;