added map_transpose

merged

attempt to move desymbolization to translation

added a somehow clueless comment

repair mess produced by resolution afterwards

using certify_instantiate

merged

cleaned up variable desymbolification and argument expansion

more appropriate printing of function terms

improved handling of parameters

path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples

towards proper handling of argument order in comprehensions

cleaned up

termT and term_of_const

added bij lemmas

new lemma bij_comp

refined mac-poly64 tests;

tuned spacing of sections; reduced line length;

more platforms;

tuned header; visible text instead of source comments;

misc changes to SOS by Philipp Meyer: CSDP_EXE as central setting; separate component src/HOL/Library/Sum_Of_Squares; misc tuning and rearrangement of neos_csdp_client; more robust treatment of shell paths; debugging depends on local flag; removed unused parts;

settings for ATP_Manager component;

merged

SUBPROOF: recovered Goal.check_finished; tuned;

added Isabelle_System.components;

src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;

etc/components; isabelle makeall operates on all components with IsaMakefile;

turned object-logics into components; isabelle makeall: operate on all components with IsaMakefile, not just hardwired "logics";

spelling;

tuned "Bootstrapping the environment"; added "Additional components";

change IFS only locally -- thanks to bash arrays;

more uniform handling of ISABELLE_HOME_USER component; discontinued ISABELLE_IGNORE_USER_SETTINGS (ever used? cf. c567f9fd61a2);

options for more precise performance figures of at-poly, which happens to run on macbroy21;

removing tracing messages in predicate compiler

improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging

commented rpred compilation; tuned

added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning

tuned proof procedure; added size-limiting predicate compilation of higher order predicates; added guessing of number parameters for registrating predicates; removed debug messages

changed resolving depending predicates and fetching in the predicate compiler

refactoring predicate compiler; repaired proof procedure to handle all test cases

refactoring predicate compiler; added type synonyms and functions split_smode and split_mode

adapted predicate compiler for quickcheck generators; added compilation of depth-limited search functions for predicates

extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures

imported patch changed mode inference of predicate compiler to return infered dataflow

imported patch generic compilation of predicate compiler with different monads

exported functions for quickcheck generator; renamed type constructing functions to fit with the type name in the Predicate theory

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;

tuned;

Task_Queue.dequeue: explicit thread;

more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;

interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);

misc tuning;

tuned

moved obsolete same_fst to Recdef.thy

adapted doc to type of "op O"

merged

merged