Sat, 06 Dec 2008 00:04:44 +0100 wenzelm improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
Sat, 06 Dec 2008 00:03:28 +0100 wenzelm excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
Sat, 06 Dec 2008 00:02:11 +0100 wenzelm added new_task;
Sat, 06 Dec 2008 00:01:57 +0100 wenzelm added constant value;
Fri, 05 Dec 2008 20:38:40 +0100 wenzelm refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises);
Fri, 05 Dec 2008 18:15:52 +0100 wenzelm uniform treatment of ISABELLE_HOME/contrib vs. ISABELLE_HOME/..;
Fri, 05 Dec 2008 11:42:27 +0100 ballarin Merged.
Fri, 05 Dec 2008 11:26:07 +0100 ballarin Interpretation in theories including interaction with subclass relation.
Fri, 05 Dec 2008 08:05:14 +0100 haftmann merged
Fri, 05 Dec 2008 08:04:53 +0100 haftmann dropped NameSpace.declare_base
Thu, 04 Dec 2008 18:37:46 -0800 huffman fix proofs
Thu, 04 Dec 2008 16:44:37 -0800 huffman merged.
Thu, 04 Dec 2008 16:28:09 -0800 huffman revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
Thu, 04 Dec 2008 16:05:45 -0800 huffman remove duplicated lemmas
Thu, 04 Dec 2008 13:30:09 -0800 huffman include iszero_simps in lemmas comp_arith
Thu, 04 Dec 2008 12:32:38 -0800 huffman add named lemma lists: neg_simps and iszero_simps
Thu, 04 Dec 2008 11:14:24 -0800 huffman change arith_special simps to avoid using neg
Fri, 05 Dec 2008 11:35:07 +1100 kleing merged
Fri, 05 Dec 2008 11:33:03 +1100 kleing run test for sunbroy2 on /tmp,
Fri, 05 Dec 2008 00:23:37 +0100 wenzelm merged
Thu, 04 Dec 2008 23:46:20 +0100 wenzelm refined Future.fork interfaces, no longer export Future.future;
Thu, 04 Dec 2008 23:46:20 +0100 wenzelm fork/map: no inheritance of group (structure is nested, not parallel);
Thu, 04 Dec 2008 23:02:56 +0100 wenzelm future proofs: pass actual futures to facilitate composite computations;
Thu, 04 Dec 2008 23:02:52 +0100 wenzelm renamed type Lazy.T to lazy;
Thu, 04 Dec 2008 23:02:46 +0100 wenzelm future_scheduler: no global task group, exceptions via collective join;
Thu, 04 Dec 2008 23:01:11 +0100 wenzelm renamed type Lazy.T to lazy;
Thu, 04 Dec 2008 23:01:03 +0100 wenzelm excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
Thu, 04 Dec 2008 23:00:58 +0100 wenzelm future proofs: pass actual futures to facilitate composite computations;
Thu, 04 Dec 2008 23:00:27 +0100 wenzelm renamed type Future.T to future;
Thu, 04 Dec 2008 23:00:21 +0100 wenzelm renamed type Lazy.T to lazy;
Thu, 04 Dec 2008 09:12:41 -0800 huffman merged.
Thu, 04 Dec 2008 08:47:45 -0800 huffman change more lemmas to avoid using iszero
Wed, 03 Dec 2008 22:16:20 -0800 huffman change some lemmas to avoid using iszero
Wed, 03 Dec 2008 21:50:36 -0800 huffman enable eq_bin_simps for simplifying equalities on numerals
Thu, 04 Dec 2008 14:44:07 +0100 haftmann merged
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Thu, 04 Dec 2008 14:17:36 +0100 nipkow NEWS
Wed, 03 Dec 2008 21:00:39 -0800 huffman fix proofs related to simplification of inequalities on numerals
Wed, 03 Dec 2008 20:45:42 -0800 huffman enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
Wed, 03 Dec 2008 20:24:17 -0800 huffman simplify proof of less_nat_number_of
Wed, 03 Dec 2008 15:04:37 -0800 huffman merged.
Wed, 03 Dec 2008 15:00:50 -0800 huffman fixed proofs due to changes in Int.thy
Wed, 03 Dec 2008 14:23:03 -0800 huffman cleaned up subsection headings;
Wed, 03 Dec 2008 21:22:38 +0100 wenzelm sources are not executable;
Wed, 03 Dec 2008 21:15:46 +0100 wenzelm eliminated traces of old Distribution directory;
Wed, 03 Dec 2008 21:02:20 +0100 wenzelm merged
Wed, 03 Dec 2008 21:02:12 +0100 wenzelm remove *.lof as well;
Wed, 03 Dec 2008 15:59:56 +0100 haftmann merged
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Wed, 03 Dec 2008 15:27:41 +0100 ballarin Sublocale: removed public after_qed; identifiers private to NewLocale.
Wed, 03 Dec 2008 15:26:46 +0100 ballarin Made global_note_qualified public.
Wed, 03 Dec 2008 14:02:24 +0000 webertj more examples
Wed, 03 Dec 2008 09:53:58 +0100 haftmann fixed typo
Wed, 03 Dec 2008 09:51:35 +0100 haftmann unfold_locales is default method - no need for explicit references
Tue, 02 Dec 2008 17:50:39 +0100 wenzelm Automated merge with file:///mnt/home/isabelle-repository/repos/isabelle
Tue, 02 Dec 2008 14:29:12 +0100 berghofe Corrected imports.
Mon, 01 Dec 2008 15:36:48 -0800 huffman clean up imports related to ContNotDenum
Mon, 01 Dec 2008 22:00:38 +0100 wenzelm ignore aux stuff in doc-src;
Mon, 01 Dec 2008 19:42:26 +0100 haftmann merged
Mon, 01 Dec 2008 19:41:16 +0100 haftmann new Binding module
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip