tuned;

tuned comments;

replaced Source.of_list_limited by slightly more economic Source.of_string_limited;

deps_thy/load_thy: store compact text to reduce space by factor 12;

make SML/NJ happy, by adhoc type-constraints;

recovered benchmarks, which are not tested automatically;

made SML/NJ happy;

merged

abstract visualization of locale ingredients; all_locales yields proper locale identifiers

tuned

accomodate for scope of "as" binding in ML

tuned code

datatype classes are abstract

avoid deprecation

robustified metis proof

modernized abel_cancel simproc setup

keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup

diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq

diff_minus subsumes diff_def

tuned whitespace

dropped essentially ineffective tuning

discontinued pretending that abel_cancel is logic-independent; cleaned up junk

merged

merged

distinguish different classes of const syntax

Scala: subtle difference in printing strings vs. complex mixfix syntax

check code generation for Scala

dropped superfluous prefixes

optional break

consolidate const_syntax naming

recovered benchmarks, which are not tested automatically;

reactivate SML/NJ test on macbroy28, while macbroy23 is unavailable;

eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing; misc tuning and simplification;

moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;

replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;

thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;

explicit dependency on theory HOL;

ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state; recovered @{theory_ref NAME} (cf. 1f09a22a1027);

added Context.get_theory -- avoid referring to accidental theory loader state (cf. Thy_Info.get_theory);

thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;

clarified/exported Future.worker_subgroup, which is already the default for Future.fork;

qualified Thy_Info.get_theory;

discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;

further Mac OS X deviations;

warning in proper transaction context;

SML/NJ: refrain from modifying toplevel pp for type string -- unclear if it could work here;

avoid duplicate printing of 'theory' state (cf. 173974e07dea);

toplevel pp for Proof.state and Toplevel.state;

execute document version at high priority;

Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;

edit_document: join parent execution in synchronous/uninterruptible mode, to prevent spurious interrupts when cascaded executions run into each other;

back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c); cancel passive tasks more actively via Exn.Interrupt, by treating them like ragular jobs here; attempts to re-assign canceled futures/promises raise Exn.Interrupt; tuned;

export Graph.get_entry for convenience;

eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that; tuned some error messages;

tuned;

observe follow_caret (again);

Session: predefined real time parameters; Document_View: delayed caret handling, for improved reactivity; selected_command: proper_command_at ignores ignored commands;

bind and then latex symbols

minor update of dependencies;

corrected range chec

first roughly working version of Imperative HOL for Scala

tuned

merged

a first sketch for Imperative HOL witht Scala

don't fail gracefully

restored long-broken syntax sanity checks

tuned interpunctation

fragments of Scala

merged

adjusted; fixed typo

dropped spurious export_code

use different log server (macbroy23 down)

more consistent spacing in generated monadic code

braced needed in layout-insensitive syntax

repaired some implementations of imperative operations

repaired reference implementation for OCaml

part of pervasive test

avoid ambiguities; tuned

repaired of_list implementation for SML, OCaml

avoid export_code ... file -

explicit optional checking

added Isar syntax for code checking

corrected import

use generic description slot for formal code checking

formal slot for code checker

export_code without file prints to standard output

check without explicit path

load cache_io before code generator; moved adhoc-overloading to generic tools

tuned infix syntax

dropped M suffix; added predicate monad bind

self-built symbol for part of bind operator

redirect stderr to stdout

merged

merged

corrected mixfix declarations and tidied proofs

merged

Fixed syntax and tidied some proofs

correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)

consolidated names of theorems

qualified names for (really) all array operations

canonical argument order for get

qualified names for (almost) all array operations

canonical argument order for present

canonical argument order for length

merged

new crontab

merged

proper merge of operation changes and generic do-syntax

merged

hide_const; update replaces change

remove separate afp settings again, use plain mac-poly64-M4 instead.

merged

new settings for afp test

Heap_Monad uses Monad_Syntax

State_Monad uses Monad_Syntax

uniform do notation for monads

generic ad-hoc overloading via check/uncheck

corrected title

theorem collections do not contain default rules any longer

fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions; added tests for Ball/Bex