huffman [Mon, 12 Jan 2009 22:16:35 -0800] rev 29462
add lemmas poly_power, poly_roots_finite
huffman [Mon, 12 Jan 2009 12:10:41 -0800] rev 29461
declare dvd_minus_iff and minus_dvd_iff [iff]
huffman [Mon, 12 Jan 2009 12:09:54 -0800] rev 29460
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
wenzelm [Tue, 13 Jan 2009 13:47:35 +0100] rev 29459
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm [Tue, 13 Jan 2009 13:46:30 +0100] rev 29458
export list;
huffman [Mon, 12 Jan 2009 10:09:23 -0800] rev 29457
correctness and uniqueness of synthetic division
huffman [Mon, 12 Jan 2009 09:35:15 -0800] rev 29456
add synthetic division algorithm for polynomials
huffman [Mon, 12 Jan 2009 09:04:25 -0800] rev 29455
add list-style syntax for pCons
huffman [Mon, 12 Jan 2009 08:46:07 -0800] rev 29454
add recursion combinator poly_rec; define poly function using poly_rec
huffman [Mon, 12 Jan 2009 08:15:07 -0800] rev 29453
add lemmas degree_{add,diff}_less
wenzelm [Sun, 11 Jan 2009 21:50:05 +0100] rev 29452
merged
huffman [Sun, 11 Jan 2009 12:05:50 -0800] rev 29451
new theory of polynomials
wenzelm [Sun, 11 Jan 2009 21:49:59 +0100] rev 29450
tuned categories;
wenzelm [Sun, 11 Jan 2009 20:40:09 +0100] rev 29449
added outer_keyword.scala: Isar command keyword classification;
wenzelm [Sun, 11 Jan 2009 18:18:35 +0100] rev 29448
added Goal.future_enabled abstraction -- now also checks that this is already
a future task, which excludes interactive commands of the old toplevel;
wenzelm [Sun, 11 Jan 2009 17:34:02 +0100] rev 29447
load main entry points sequentially, for reduced memory demands;
wenzelm [Sun, 11 Jan 2009 16:56:59 +0100] rev 29446
merged
wenzelm [Sun, 11 Jan 2009 14:23:54 +0100] rev 29445
merged
wenzelm [Sun, 11 Jan 2009 16:41:48 +0100] rev 29444
less ambitious ML_OPTIONS;
wenzelm [Sun, 11 Jan 2009 14:22:34 +0100] rev 29443
merged
haftmann [Sun, 11 Jan 2009 14:18:32 +0100] rev 29442
merged
haftmann [Sun, 11 Jan 2009 14:18:17 +0100] rev 29441
explicit bookkeeping of intro rules and axiom
haftmann [Sun, 11 Jan 2009 14:18:16 +0100] rev 29440
stripped Id
haftmann [Sun, 11 Jan 2009 14:18:16 +0100] rev 29439
construct explicit class morphism
wenzelm [Sun, 11 Jan 2009 13:48:11 +0100] rev 29438
less ambitious ML_OPTIONS;
wenzelm [Sat, 10 Jan 2009 23:56:11 +0100] rev 29437
schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
wenzelm [Sat, 10 Jan 2009 21:47:02 +0100] rev 29436
future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
wenzelm [Sat, 10 Jan 2009 21:32:30 +0100] rev 29435
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
wenzelm [Sat, 10 Jan 2009 16:58:56 +0100] rev 29434
remove_thy: perform PureThy.cancel_proofs;
schedule_futures: PureThy.join_proofs before after_load -- achieves parallel error messages;
wenzelm [Sat, 10 Jan 2009 16:55:46 +0100] rev 29433
added cancel_proofs, based on task groups of "entered" proofs;
wenzelm [Sat, 10 Jan 2009 16:54:55 +0100] rev 29432
added pending_groups -- accumulates task groups of local derivations only;
wenzelm [Sat, 10 Jan 2009 16:53:12 +0100] rev 29431
added cancel_group;
wenzelm [Sat, 10 Jan 2009 16:00:34 +0100] rev 29430
merged
wenzelm [Sat, 10 Jan 2009 13:11:56 +0100] rev 29429
schedule_futures: tuned final consolidation, explicit after_load phase;
wenzelm [Sat, 10 Jan 2009 13:10:38 +0100] rev 29428
load_thy: explicit after_load phase for presentation;
wenzelm [Sat, 10 Jan 2009 13:10:07 +0100] rev 29427
excursion: commit_exit internally -- checkpoints are fully persistent now;
excursion: do not force intermediate result states yet -- great performance improvement;
wenzelm [Sat, 10 Jan 2009 15:55:19 +0100] rev 29426
slightly more robust matching of session name;
wenzelm [Sat, 10 Jan 2009 01:28:31 +0100] rev 29425
merged
wenzelm [Sat, 10 Jan 2009 01:06:32 +0100] rev 29424
fixed proof involving dvd;
wenzelm [Sat, 10 Jan 2009 01:28:18 +0100] rev 29423
tuned;
wenzelm [Sat, 10 Jan 2009 01:28:03 +0100] rev 29422
added force_result;
wenzelm [Sat, 10 Jan 2009 00:25:31 +0100] rev 29421
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
wenzelm [Sat, 10 Jan 2009 00:24:07 +0100] rev 29420
simplified join_proofs;
wenzelm [Fri, 09 Jan 2009 23:39:53 +0100] rev 29419
merged
wenzelm [Fri, 09 Jan 2009 23:34:36 +0100] rev 29418
added split_thy_path;
wenzelm [Fri, 09 Jan 2009 23:33:59 +0100] rev 29417
added running task markup;
wenzelm [Thu, 08 Jan 2009 13:18:34 +0100] rev 29416
tuned;
wenzelm [Thu, 08 Jan 2009 12:15:23 +0100] rev 29415
merged
wenzelm [Fri, 09 Jan 2009 19:41:33 +0100] rev 29414
merged
huffman [Fri, 09 Jan 2009 09:49:01 -0800] rev 29413
merged.
huffman [Fri, 09 Jan 2009 09:34:49 -0800] rev 29412
fix proof broken by changes in dvd theory
huffman [Thu, 08 Jan 2009 21:13:40 -0800] rev 29411
merged.
huffman [Thu, 08 Jan 2009 12:25:22 -0800] rev 29410
remove type-specific proofs
huffman [Thu, 08 Jan 2009 10:43:09 -0800] rev 29409
add lemma dvd_diff to class comm_ring_1
huffman [Thu, 08 Jan 2009 10:26:50 -0800] rev 29408
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
huffman [Thu, 08 Jan 2009 10:07:39 -0800] rev 29407
move lemmas mult_minus{left,right} inside class ring
huffman [Thu, 08 Jan 2009 09:58:36 -0800] rev 29406
clean up division_ring proofs
huffman [Thu, 08 Jan 2009 09:12:29 -0800] rev 29405
add class ring_div; generalize mod/diff/minus proofs for class ring_div
huffman [Thu, 08 Jan 2009 08:36:16 -0800] rev 29404
generalize zmod_zmod_cancel -> mod_mod_cancel
huffman [Thu, 08 Jan 2009 08:24:08 -0800] rev 29403
generalize some div/mod lemmas; remove type-specific proofs