2008-12-27 krauss 2008-12-27 tuned NEWS; CONTRIBUTORS
2008-12-27 krauss 2008-12-27 renamed LexOrds.thy to Termination.thy; examples for sizechange method
2008-12-27 wenzelm 2008-12-27 tuned;
2008-12-27 wenzelm 2008-12-27 merged
2008-12-27 wenzelm 2008-12-27 refined execute, which replaces exec/exec2;
2008-12-27 wenzelm 2008-12-27 maintain initial process environment; refined execute, which replaces exec/exec2; tuned;
2008-12-27 haftmann 2008-12-27 merged
2008-12-27 haftmann 2008-12-27 tackling simultaneous val/fun bindings
2008-12-27 wenzelm 2008-12-27 proper class IsabelleSystem -- no longer static; tuned;
2008-12-27 wenzelm 2008-12-27 PATH: /opt/local/bin is back again (required for latex etc.);
2008-12-24 huffman 2008-12-24 merged.
2008-12-24 huffman 2008-12-24 clean up lemmas about ln
2008-12-24 huffman 2008-12-24 clean up lemmas about exp
2008-12-24 huffman 2008-12-24 more proofs about differentiable
2008-12-24 huffman 2008-12-24 use less_iff_Suc_add instead of less_add_one
2008-12-24 huffman 2008-12-24 rearranged subsections; cleaned up some proofs
2008-12-24 huffman 2008-12-24 move theorems about limits from Transcendental.thy to Deriv.thy
2008-12-24 huffman 2008-12-24 cleaned up some proofs; removed redundant simp rules
2008-12-23 huffman 2008-12-23 move sin and cos to their own subsection
2008-12-23 huffman 2008-12-23 clean up some proofs; remove unused lemmas
2008-12-23 wenzelm 2008-12-23 tuned;
2008-12-23 wenzelm 2008-12-23 * Proofs of are run in parallel on multi-core systems; * High-level support for concurrent ML programming;
2008-12-23 wenzelm 2008-12-23 updated generated file;
2008-12-23 wenzelm 2008-12-23 updated thread-safe programming;
2008-12-23 wenzelm 2008-12-23 updated generated file;
2008-12-23 wenzelm 2008-12-23 added float_token, and num_const, float_const; tuned;
2008-12-23 wenzelm 2008-12-23 renamed terminal category "float" to "float_token", to avoid name space conflicts with actual "float" types in user theories (only "float_const" is encountered in practice anyway); tuned;
2008-12-23 wenzelm 2008-12-23 manual file type setup using AppHack 1.1;
2008-12-23 wenzelm 2008-12-23 target PWD;
2008-12-23 wenzelm 2008-12-23 updated scala path;
2008-12-23 wenzelm 2008-12-23 added platform_file; added find_logics;
2008-12-22 wenzelm 2008-12-22 proper -X option; relative result, do not insist in "$THIS/Isabelle.app";
2008-12-22 wenzelm 2008-12-22 unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result; tuned;
2008-12-22 wenzelm 2008-12-22 more sophisticated MacOS interface script (mostly for Carbon Emacs); no longer include MacPorts path; simplified default PROOFGENERAL_OPTIONS, removed PROOFGENERAL_EMACS;
2008-12-21 wenzelm 2008-12-21 updated web style for Mercurial 1.1.1;
2008-12-21 wenzelm 2008-12-21 misc webstyle adaptions;
2008-12-20 wenzelm 2008-12-20 updated web style for Mercurial 1.1;
2008-12-20 wenzelm 2008-12-20 removed Ids;
2008-12-20 wenzelm 2008-12-20 merged
2008-12-20 wenzelm 2008-12-20 removed Ids;
2008-12-19 huffman 2008-12-19 merged.
2008-12-18 huffman 2008-12-18 constdefs -> definition
2008-12-19 wenzelm 2008-12-19 removed Ids;
2008-12-18 huffman 2008-12-18 merged.
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-12-17 wenzelm 2008-12-17 merged
2008-12-17 wenzelm 2008-12-17 basic setup for MacOS application bundle;
2008-12-17 haftmann 2008-12-17 GHC ext pragma in generated Haskell modules
2008-12-17 haftmann 2008-12-17 dropped Ids
2008-12-17 haftmann 2008-12-17 temporary adaption to new locale code
2008-12-17 haftmann 2008-12-17 restructured; circumvent sort problem
2008-12-16 huffman 2008-12-16 merged.
2008-12-16 huffman 2008-12-16 new theory Dsum: cpo of disjoint sum
2008-12-16 huffman 2008-12-16 scale dependency graph in document
2008-12-16 Christian Urban 2008-12-16 changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
2008-12-16 wenzelm 2008-12-16 proper document antiquotations;
2008-12-16 wenzelm 2008-12-16 merged
2008-12-16 krauss 2008-12-16 method "sizechange" proves termination of functions; added more infrastructure for termination proofs
2008-12-16 wenzelm 2008-12-16 future proofs: Future.fork_pri 1 minimizes queue length and pending promises -- slight improvement of throughput, at the cost of a bit of parallelism;
2008-12-16 wenzelm 2008-12-16 renamed structure TaskQueue to Task_Queue;