2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-23 wenzelm 2009-07-23 use regular Display.string_of_thm_global;
2009-07-23 wenzelm 2009-07-23 tuned ML_OPTIONS;
2009-07-23 haftmann 2009-07-23 fixed doc
2009-07-23 berghofe 2009-07-23 Purely functional type inference.
2009-07-22 haftmann 2009-07-22 merged
2009-07-22 haftmann 2009-07-22 moved complete_lattice &c. into separate theory
2009-07-22 Christian Urban 2009-07-22 merged
2009-07-22 Christian Urban 2009-07-22 tuned proofs and added some lemmas
2009-07-22 haftmann 2009-07-22 merged
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union
2009-07-22 haftmann 2009-07-22 spurious proof failure
2009-07-22 wenzelm 2009-07-22 original rail implementation by Michael Kerscher;
2009-07-22 wenzelm 2009-07-22 merged, resolving trivial conflict;
2009-07-22 nipkow 2009-07-22 News
2009-07-22 haftmann 2009-07-22 explicit antiquotation
2009-07-21 haftmann 2009-07-21 merged
2009-07-21 haftmann 2009-07-21 merged
2009-07-21 haftmann 2009-07-21 obey captialized directory names convention
2009-07-21 haftmann 2009-07-21 dropped ancient flat_names option
2009-07-21 haftmann 2009-07-21 dropped ancient flat_names option
2009-07-21 haftmann 2009-07-21 integrated add_triv_classes into evaluation stack
2009-07-21 haftmann 2009-07-21 more accurate check of judgment type
2009-07-21 haftmann 2009-07-21 UNIV_code now named UNIV_apply
2009-07-21 haftmann 2009-07-21 attempt for more concise setup of non-etacontracting binders
2009-07-21 haftmann 2009-07-21 moved abstract algebra section to the end
2009-07-21 haftmann 2009-07-21 merged
2009-07-21 haftmann 2009-07-21 Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
2009-07-21 haftmann 2009-07-21 merged
2009-07-21 haftmann 2009-07-21 swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
2009-07-20 haftmann 2009-07-20 merged
2009-07-20 haftmann 2009-07-20 dropped add_registration interface in locale
2009-07-21 nipkow 2009-07-21 Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM
2009-07-21 nipkow 2009-07-21 Tests for executability of "prime"
2009-07-22 wenzelm 2009-07-22 less ambitious settings;
2009-07-22 wenzelm 2009-07-22 future_job: more robust Exn.capture outside thread attribute change;
2009-07-22 wenzelm 2009-07-22 shutdown future scheduler after (failed) SAT_Examples, to workaround interference problem with follow-up theory loading;
2009-07-21 wenzelm 2009-07-21 future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group; control combinators: paranoia eta-expansion to ensure proper operational semantics;
2009-07-21 wenzelm 2009-07-21 maintain Future.worker_group as management data; cancel_thy: refer to proper task group; tuned;
2009-07-21 wenzelm 2009-07-21 join_proofs: implicit exception; removed obsolete cancel_proofs, cf. cancel_thy in thy_info.ML; tuned;
2009-07-21 wenzelm 2009-07-21 simultaneous join_proofs; removed obsolete promises_of;
2009-07-21 wenzelm 2009-07-21 map: subgroup of worker_group;
2009-07-21 wenzelm 2009-07-21 added worker_group; fork: default to subgroup of worker_group; removed obsolete fork_local; join/get_result: cumulative flattened exceptions; map: subgroup of worker_group;
2009-07-21 wenzelm 2009-07-21 support for nested groups -- cancellation is propagated to peers and subgroups; added is_canceled; tuned;
2009-07-21 wenzelm 2009-07-21 added flatten/flatten_list -- supercedes internal plain_exns; represent empty failure as EXCEPTIONS [] instead of Interrupt;
2009-07-21 wenzelm 2009-07-21 propagate exceptions within future groups; Future.map: inherit group;
2009-07-21 wenzelm 2009-07-21 less ambitious ML_OPTIONS;
2009-07-21 wenzelm 2009-07-21 disabled macbroy6 -- hardware repair;
2009-07-21 wenzelm 2009-07-21 tuned;
2009-07-21 wenzelm 2009-07-21 tuned tracing; provide spare worker threads to saturate hardware while other workers wait during join;
2009-07-21 wenzelm 2009-07-21 prefer simultaneous join -- for improved scheduling;
2009-07-21 wenzelm 2009-07-21 tuned dequeu_towards: try immediate tasks before expensive all_preds;
2009-07-21 wenzelm 2009-07-21 Display.pretty_thm now requires a proper context;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-21 wenzelm 2009-07-21 moved ProofContext.pretty_thm to Display.pretty_thm etc.; explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.; removed some very old thm print operations;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-07-20 wenzelm 2009-07-20 removed obsolete CVS Ids;
2009-07-20 wenzelm 2009-07-20 merged
2009-07-20 haftmann 2009-07-20 merged