| 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
|
| Wed, 03 Dec 2008 20:45:42 -0800 |
huffman |
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
|
changeset |
files
|
| Wed, 03 Dec 2008 20:24:17 -0800 |
huffman |
simplify proof of less_nat_number_of
|
changeset |
files
|
| Wed, 03 Dec 2008 15:04:37 -0800 |
huffman |
merged.
|
changeset |
files
|
| Wed, 03 Dec 2008 15:00:50 -0800 |
huffman |
fixed proofs due to changes in Int.thy
|
changeset |
files
|
| Wed, 03 Dec 2008 14:23:03 -0800 |
huffman |
cleaned up subsection headings;
|
changeset |
files
|
| Wed, 03 Dec 2008 21:22:38 +0100 |
wenzelm |
sources are not executable;
|
changeset |
files
|
| Wed, 03 Dec 2008 21:15:46 +0100 |
wenzelm |
eliminated traces of old Distribution directory;
|
changeset |
files
|
| Wed, 03 Dec 2008 21:02:20 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 03 Dec 2008 21:02:12 +0100 |
wenzelm |
remove *.lof as well;
|
changeset |
files
|
| Wed, 03 Dec 2008 15:59:56 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
changeset |
files
|
| Wed, 03 Dec 2008 15:27:41 +0100 |
ballarin |
Sublocale: removed public after_qed; identifiers private to NewLocale.
|
changeset |
files
|
| Wed, 03 Dec 2008 15:26:46 +0100 |
ballarin |
Made global_note_qualified public.
|
changeset |
files
|
| Wed, 03 Dec 2008 14:02:24 +0000 |
webertj |
more examples
|
changeset |
files
|
| Wed, 03 Dec 2008 09:53:58 +0100 |
haftmann |
fixed typo
|
changeset |
files
|
| Wed, 03 Dec 2008 09:51:35 +0100 |
haftmann |
unfold_locales is default method - no need for explicit references
|
changeset |
files
|
| Tue, 02 Dec 2008 17:50:39 +0100 |
wenzelm |
Automated merge with file:///mnt/home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Tue, 02 Dec 2008 14:29:12 +0100 |
berghofe |
Corrected imports.
|
changeset |
files
|
| Mon, 01 Dec 2008 15:36:48 -0800 |
huffman |
clean up imports related to ContNotDenum
|
changeset |
files
|
| Mon, 01 Dec 2008 22:00:38 +0100 |
wenzelm |
ignore aux stuff in doc-src;
|
changeset |
files
|
| Mon, 01 Dec 2008 19:42:26 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 01 Dec 2008 19:41:16 +0100 |
haftmann |
new Binding module
|
changeset |
files
|
| Mon, 01 Dec 2008 16:02:57 +0100 |
haftmann |
Locale.*note* with conventional argument type
|
changeset |
files
|
| Mon, 01 Dec 2008 14:56:08 +0100 |
haftmann |
added code equation for subset
|
changeset |
files
|
| Mon, 01 Dec 2008 17:38:17 +0100 |
ballarin |
Merged again.
|
changeset |
files
|
| Mon, 01 Dec 2008 17:37:02 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Mon, 01 Dec 2008 16:59:31 +0100 |
ballarin |
No resolution of patterns within context statements.
|
changeset |
files
|
| Tue, 02 Dec 2008 17:50:25 +0100 |
wenzelm |
removed CVS Id;
|
changeset |
files
|
| Mon, 01 Dec 2008 17:48:12 +0100 |
wenzelm |
proper check of ISABELLE_TOOLS directories;
|
changeset |
files
|
| Mon, 01 Dec 2008 17:32:40 +0100 |
wenzelm |
removed obsolete tags (leftover from old CVS branches);
|
changeset |
files
|
| Mon, 01 Dec 2008 17:07:06 +0100 |
wenzelm |
makedist -- make Isabelle source distribution (Mercurial version);
|
changeset |
files
|
| Mon, 01 Dec 2008 15:22:17 +0100 |
wenzelm |
renamed makedist_mercurial to makedist, deleting the old version;
|
changeset |
files
|
| Mon, 01 Dec 2008 14:46:27 +0100 |
wenzelm |
updated to python2.5;
|
changeset |
files
|
| Mon, 01 Dec 2008 14:42:24 +0100 |
wenzelm |
convert to isabelle-cvs, the old version;
|
changeset |
files
|
| Mon, 01 Dec 2008 14:41:13 +0100 |
wenzelm |
adapted description: old CVS;
|
changeset |
files
|
| Mon, 01 Dec 2008 13:43:32 +0100 |
ballarin |
Methods intro_locales and unfold_locales apply to both old and new locales.
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:04 +0100 |
haftmann |
code_include with attach
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:03 +0100 |
haftmann |
experimental implementation of a well-sorting algorithm
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:02 +0100 |
haftmann |
code_funcgr interface includes also sort algebra
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:01 +0100 |
haftmann |
exported get_accesses (for diagnostic purpose)
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:00 +0100 |
haftmann |
more means for algebra projection
|
changeset |
files
|
| Mon, 01 Dec 2008 12:16:59 +0100 |
haftmann |
consider TeX spacing conventions for punctuation marks
|
changeset |
files
|
| Sun, 30 Nov 2008 18:10:00 +0100 |
huffman |
fix typed print translation for card UNIV
|
changeset |
files
|
| Sun, 30 Nov 2008 16:00:16 +0100 |
wenzelm |
removed obsolete CVS instructions;
|
changeset |
files
|
| Sun, 30 Nov 2008 15:03:47 +0100 |
wenzelm |
fixed spelling;
|
changeset |
files
|
| Sun, 30 Nov 2008 14:43:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|