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;
2008-12-16 wenzelm 2008-12-16 Future.fork_pri;
2008-12-16 wenzelm 2008-12-16 renamed structure TaskQueue to Task_Queue; tasks are ordered according to priority, which has been generalized from bool to int; removed unused focus; tuned dequeue: single pass due to proper priority order; tuned dequeue_towards;
2008-12-16 wenzelm 2008-12-16 renamed structure TaskQueue to Task_Queue;
2008-12-16 wenzelm 2008-12-16 renamed structure TaskQueue to Task_Queue; generalized fork_background to fork_pri; reduced tracing; map: inherit task priority; removed unused focus;
2008-12-16 wenzelm 2008-12-16 removed old scheduler;
2008-12-16 wenzelm 2008-12-16 tuned enqueue: plain add_edge, acyclic not required here;
2008-12-15 wenzelm 2008-12-15 tuned messages;
2008-12-15 wenzelm 2008-12-15 updated generated file;
2008-12-15 wenzelm 2008-12-15 repaired railroad accident;
2008-12-15 wenzelm 2008-12-15 updated generated files;
2008-12-15 wenzelm 2008-12-15 added 'atp_messages' command, which displays recent messages synchronously;
2008-12-15 nipkow 2008-12-15 merged
2008-12-15 nipkow 2008-12-15 flipped fold implementation
2008-12-11 nipkow 2008-12-11 merged
2008-12-11 nipkow 2008-12-11 codegen
2008-12-11 nipkow 2008-12-11 code for {x:A. P(x)} and for fold
2008-12-11 nipkow 2008-12-11 Testfile for Stefan's code generator
2008-12-15 haftmann 2008-12-15 moved value.ML to src/Tools
2008-12-15 haftmann 2008-12-15 \underscoreoff is now default
2008-12-15 Christian Urban 2008-12-15 tuned some proofs
2008-12-13 wenzelm 2008-12-13 removed Ids;
2008-12-13 berghofe 2008-12-13 merged
2008-12-13 berghofe 2008-12-13 merged
2008-12-13 berghofe 2008-12-13 merged
2008-12-13 berghofe 2008-12-13 Unified syntax of nominal_primrec with the one used by fun(ction) and new version of primrec command.
2008-12-13 berghofe 2008-12-13 Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.
2008-12-13 wenzelm 2008-12-13 merged
2008-12-13 wenzelm 2008-12-13 tuned comments; tuned;
2008-12-13 wenzelm 2008-12-13 tuned ML_OPTIONS for improved multicore performance;
2008-12-13 wenzelm 2008-12-13 refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry; tuned history: renamed version to stage, disallow checkpoint/finish_thy on finished theories; added display_names -- user-level presentation; removed obsolete exists_name, names_of; tuned;
2008-12-13 wenzelm 2008-12-13 requires: check ancestors directly;
2008-12-13 wenzelm 2008-12-13 Context.display_names;
2008-12-12 wenzelm 2008-12-12 global_qed: refrain from ProofContext.auto_bind_facts, to avoid polluting the final result context with bindings involving loose free variables;
2008-12-13 wenzelm 2008-12-13 usage: echo ML settings as well;
2008-12-12 wenzelm 2008-12-12 future proofs: more robust check via Future.enabled;
2008-12-11 wenzelm 2008-12-11 removed former Isabelle font (cf. IsabelleItalic);
2008-12-11 wenzelm 2008-12-11 incorporated isabelle-fonts side-branch (forced merge);