| Thu, 04 Dec 2008 18:37:46 -0800 |
huffman |
fix proofs
|
changeset |
files
|
| Thu, 04 Dec 2008 16:44:37 -0800 |
huffman |
merged.
|
changeset |
files
|
| Thu, 04 Dec 2008 16:28:09 -0800 |
huffman |
revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
|
changeset |
files
|
| Thu, 04 Dec 2008 16:05:45 -0800 |
huffman |
remove duplicated lemmas
|
changeset |
files
|
| Thu, 04 Dec 2008 13:30:09 -0800 |
huffman |
include iszero_simps in lemmas comp_arith
|
changeset |
files
|
| Thu, 04 Dec 2008 12:32:38 -0800 |
huffman |
add named lemma lists: neg_simps and iszero_simps
|
changeset |
files
|
| Thu, 04 Dec 2008 11:14:24 -0800 |
huffman |
change arith_special simps to avoid using neg
|
changeset |
files
|
| Fri, 05 Dec 2008 11:35:07 +1100 |
kleing |
merged
|
changeset |
files
|
| Fri, 05 Dec 2008 11:33:03 +1100 |
kleing |
run test for sunbroy2 on /tmp,
|
changeset |
files
|
| Fri, 05 Dec 2008 00:23:37 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 04 Dec 2008 23:46:20 +0100 |
wenzelm |
refined Future.fork interfaces, no longer export Future.future;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:46:20 +0100 |
wenzelm |
fork/map: no inheritance of group (structure is nested, not parallel);
|
changeset |
files
|
| Thu, 04 Dec 2008 23:02:56 +0100 |
wenzelm |
future proofs: pass actual futures to facilitate composite computations;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:02:52 +0100 |
wenzelm |
renamed type Lazy.T to lazy;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:02:46 +0100 |
wenzelm |
future_scheduler: no global task group, exceptions via collective join;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:01:11 +0100 |
wenzelm |
renamed type Lazy.T to lazy;
|
changeset |
files
|
| 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;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:00:58 +0100 |
wenzelm |
future proofs: pass actual futures to facilitate composite computations;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:00:27 +0100 |
wenzelm |
renamed type Future.T to future;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:00:21 +0100 |
wenzelm |
renamed type Lazy.T to lazy;
|
changeset |
files
|
| Thu, 04 Dec 2008 09:12:41 -0800 |
huffman |
merged.
|
changeset |
files
|
| Thu, 04 Dec 2008 08:47:45 -0800 |
huffman |
change more lemmas to avoid using iszero
|
changeset |
files
|
| Wed, 03 Dec 2008 22:16:20 -0800 |
huffman |
change some lemmas to avoid using iszero
|
changeset |
files
|
| Wed, 03 Dec 2008 21:50:36 -0800 |
huffman |
enable eq_bin_simps for simplifying equalities on numerals
|
changeset |
files
|
| Thu, 04 Dec 2008 14:44:07 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
changeset |
files
|
| Thu, 04 Dec 2008 14:17:36 +0100 |
nipkow |
NEWS
|
changeset |
files
|
| Wed, 03 Dec 2008 21:00:39 -0800 |
huffman |
fix proofs related to simplification of inequalities on numerals
|
changeset |
files
|