2012-10-21 haftmann 2012-10-21 more conventional argument order; dropped dead code
2012-10-21 bulwahn 2012-10-21 another refinement in the comprehension conversion
2012-10-21 bulwahn 2012-10-21 refined simplifier call in comprehension_conv
2012-10-21 bulwahn 2012-10-21 passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
2012-10-20 wenzelm 2012-10-20 avoid STIX font, which tends to render badly;
2012-10-20 wenzelm 2012-10-20 extra jar for scala-2.10.0-RC1;
2012-10-20 wenzelm 2012-10-20 more explicit auxiliary classes to avoid warning "reflective access of structural type member method" of scala-2.10.0-RC1;
2012-10-20 wenzelm 2012-10-20 avoid duplicate build of jars_fresh;
2012-10-20 wenzelm 2012-10-20 obsolete, cf. README_REPOSITORY;
2012-10-20 wenzelm 2012-10-20 accomodate scala-2.10.0-RC1;
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