formally stylized

formally stylized

corrected Pair to Char

merged

Fixed a bug where the simplifier would hang on lemma "f a = M { nat j |j. 0 <= j & j < f b}" pre_decomp/pre_tac no longer split terms that contain (non-locally) bound variables (e.g., "nat j" in the above example).

merged

Removal of redundant settings of unification trace and search bounds.

Demonstrations of sledgehammer in protocol proofs.

added PARALLEL_CHOICE, PARALLEL_GOALS;

merged

SOS: function to set default prover; output channel changed

interrupt handler for neos csdp client

clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;

updated generated document

dropped temporary adjustments to non-working eta expansion in recfun_codegen.ML

proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML

merged

temporary adjustment to dubious state of eta expansion in recfun_codegen

properly merged

same_typscheme replaces ugly common_typ_eqns

moved all technical processing of code equations to code_thingol.ML

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