accomodate scala-2.10.0-RC1;

tailored enum specification towards simple instantiation; tuned enum instantiations

refined internal structure of Enum.thy

moved quite generic material from theory Enum to more appropriate places

adding another test case for the set_comprehension_simproc to the theory in HOL/ex

improving tactic in setcomprehension_simproc

adjusting proofs

tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage

passing names and types of all bounds around in the simproc

locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree

more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;

merged

don't include Quotient_Option - workaround to a transfer bug

ignore old stuff and thus speed up the script greatly;

proper find -mtime (file data) instead of -ctime (meta data);

made SML/NJ happy;

clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.);

back to polyml-5.4.1 (cf. b3110dec1a32) -- no cause of spurious interrupts;

merged

back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;

more basic Goal.reset_futures as snapshot of implicit state; more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);

tuned proof;

update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer

tuned proofs

new theorem

merged

merged

merged

merged

fixed proof (cf. a81f95693c68);

tuned Isar output

tuned

updated docs

renamed Isar-proof related options + changed semantics of Isar shrinking

tuning

fixed theorem lookup code in Isar proof reconstruction

tuning

refactor code

tuning

more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);

collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);

more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;

tuned message;

tuned comment;

avoid spurious "bad" markup for show/test_proof; tuned;

more official Future.terminate; tuned signature;

simp results for simplification results of Inf/Sup expressions on bool; tuned proofs

no sort constraints on datatype constructors in internal bookkeeping

HOL-BNF-Examples is sequential for now, due to spurious interrupts (again);

merged

comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic

checking for bound variables in the set expression; handling negation more generally

set_comprehension_pointfree simproc now handles the complicated test case; tuned

refined conversion to only react on proper set comprehensions; tuned

moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)

employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc