2012-10-20 haftmann 2012-10-20 tailored enum specification towards simple instantiation; tuned enum instantiations
2012-10-20 haftmann 2012-10-20 refined internal structure of Enum.thy
2012-10-20 haftmann 2012-10-20 moved quite generic material from theory Enum to more appropriate places
2012-10-20 bulwahn 2012-10-20 adding another test case for the set_comprehension_simproc to the theory in HOL/ex
2012-10-20 bulwahn 2012-10-20 improving tactic in setcomprehension_simproc
2012-10-20 bulwahn 2012-10-20 adjusting proofs
2012-10-20 bulwahn 2012-10-20 tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
2012-10-20 bulwahn 2012-10-20 passing names and types of all bounds around in the simproc
2012-10-18 bulwahn 2012-10-18 locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree
2012-10-19 wenzelm 2012-10-19 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
2012-10-19 wenzelm 2012-10-19 merged
2012-10-19 kuncar 2012-10-19 don't include Quotient_Option - workaround to a transfer bug
2012-10-19 wenzelm 2012-10-19 ignore old stuff and thus speed up the script greatly;
2012-10-19 wenzelm 2012-10-19 proper find -mtime (file data) instead of -ctime (meta data);
2012-10-19 wenzelm 2012-10-19 made SML/NJ happy;
2012-10-19 wenzelm 2012-10-19 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.);
2012-10-18 wenzelm 2012-10-18 back to polyml-5.4.1 (cf. b3110dec1a32) -- no cause of spurious interrupts;
2012-10-18 wenzelm 2012-10-18 merged
2012-10-18 wenzelm 2012-10-18 back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;
2012-10-18 wenzelm 2012-10-18 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);
2012-10-18 wenzelm 2012-10-18 tuned proof;
2012-10-18 kuncar 2012-10-18 update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
2012-10-18 kuncar 2012-10-18 tuned proofs
2012-10-18 kuncar 2012-10-18 new theorem
2012-10-18 wenzelm 2012-10-18 merged
2012-10-18 wenzelm 2012-10-18 merged
2012-10-18 wenzelm 2012-10-18 merged
2012-10-18 wenzelm 2012-10-18 merged
2012-10-18 wenzelm 2012-10-18 fixed proof (cf. a81f95693c68);
2012-10-18 blanchet 2012-10-18 tuned Isar output
2012-10-18 nipkow 2012-10-18 tuned
2012-10-18 blanchet 2012-10-18 updated docs
2012-10-18 blanchet 2012-10-18 renamed Isar-proof related options + changed semantics of Isar shrinking
2012-10-18 blanchet 2012-10-18 tuning
2012-10-18 blanchet 2012-10-18 fixed theorem lookup code in Isar proof reconstruction
2012-10-18 blanchet 2012-10-18 tuning
2012-10-18 blanchet 2012-10-18 refactor code
2012-10-18 blanchet 2012-10-18 tuning
2012-10-18 wenzelm 2012-10-18 more robust future_proof result with specific error message (e.g. relevant for incomplete proof of non-registered theorem);
2012-10-18 wenzelm 2012-10-18 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);
2012-10-18 wenzelm 2012-10-18 more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;
2012-10-18 wenzelm 2012-10-18 tuned message;
2012-10-18 wenzelm 2012-10-18 tuned comment;
2012-10-18 wenzelm 2012-10-18 avoid spurious "bad" markup for show/test_proof; tuned;
2012-10-18 wenzelm 2012-10-18 more official Future.terminate; tuned signature;
2012-10-18 haftmann 2012-10-18 simp results for simplification results of Inf/Sup expressions on bool; tuned proofs
2012-10-18 haftmann 2012-10-18 no sort constraints on datatype constructors in internal bookkeeping
2012-10-17 wenzelm 2012-10-17 HOL-BNF-Examples is sequential for now, due to spurious interrupts (again);
2012-10-17 wenzelm 2012-10-17 merged
2012-10-17 bulwahn 2012-10-17 comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
2012-10-17 bulwahn 2012-10-17 checking for bound variables in the set expression; handling negation more generally
2012-10-17 bulwahn 2012-10-17 set_comprehension_pointfree simproc now handles the complicated test case; tuned
2012-10-17 bulwahn 2012-10-17 refined conversion to only react on proper set comprehensions; tuned
2012-10-17 bulwahn 2012-10-17 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)
2012-10-17 bulwahn 2012-10-17 employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
2012-10-17 wenzelm 2012-10-17 another Future.shutdown after Future.cancel_groups (cf. 0d4106850eb2);
2012-10-17 wenzelm 2012-10-17 more robust cancel_now: avoid shooting yourself in the foot;
2012-10-17 wenzelm 2012-10-17 more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;
2012-10-17 wenzelm 2012-10-17 proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
2012-10-17 wenzelm 2012-10-17 added Output "Detach" button;