2009-09-03 tuned
boehmes [Thu, 03 Sep 2009 15:47:39 +0200] rev 32509
tuned
2009-09-03 scaled avg_time
nipkow [Thu, 03 Sep 2009 15:30:05 +0200] rev 32508
scaled avg_time
2009-09-03 merged
nipkow [Thu, 03 Sep 2009 14:50:02 +0200] rev 32507
merged
2009-09-03 tuned
nipkow [Thu, 03 Sep 2009 14:49:34 +0200] rev 32506
tuned
2009-09-03 isatest: collect test results and logs in testdata repository
krauss [Thu, 03 Sep 2009 14:40:52 +0200] rev 32505
isatest: collect test results and logs in testdata repository
2009-09-03 replaced backlist by whitelist
boehmes [Thu, 03 Sep 2009 14:31:04 +0200] rev 32504
replaced backlist by whitelist
2009-09-03 Mirabelle: logging of exceptions (works only for PolyML)
boehmes [Thu, 03 Sep 2009 14:05:13 +0200] rev 32503
Mirabelle: logging of exceptions (works only for PolyML)
2009-09-02 merged
wenzelm [Wed, 02 Sep 2009 22:12:40 +0200] rev 32502
merged
2009-09-02 refined delay into delay_first/delay_last;
wenzelm [Wed, 02 Sep 2009 22:12:20 +0200] rev 32501
refined delay into delay_first/delay_last;
2009-09-02 merged
boehmes [Wed, 02 Sep 2009 21:34:13 +0200] rev 32500
merged
2009-09-02 add report script for Mirabelle
boehmes [Wed, 02 Sep 2009 21:33:16 +0200] rev 32499
add report script for Mirabelle
2009-09-02 Mirabelle: actions are responsible for handling exceptions,
boehmes [Wed, 02 Sep 2009 21:31:58 +0200] rev 32498
Mirabelle: actions are responsible for handling exceptions, Mirabelle core logs only structural information, measuring running times for sledgehammer and subsequent metis invocation, Mirabelle produces reports for every theory (only for sledgehammer at the moment)
2009-09-02 removed errors overseen in previous changes
boehmes [Wed, 02 Sep 2009 16:29:50 +0200] rev 32497
removed errors overseen in previous changes
2009-09-02 moved Mirabelle from HOL/Tools to HOL,
boehmes [Wed, 02 Sep 2009 16:23:53 +0200] rev 32496
moved Mirabelle from HOL/Tools to HOL, added session HOL-Mirabelle
2009-09-02 removed unused signature
boehmes [Wed, 02 Sep 2009 16:02:37 +0200] rev 32495
removed unused signature
2009-09-02 explicit checks;
wenzelm [Wed, 02 Sep 2009 20:49:04 +0200] rev 32494
explicit checks;
2009-09-02 updated Poly/ML SVN version;
wenzelm [Wed, 02 Sep 2009 17:33:25 +0200] rev 32493
updated Poly/ML SVN version;
2009-09-02 eval/location_props: always produce YXML markup, independent of print_mode;
wenzelm [Wed, 02 Sep 2009 16:51:19 +0200] rev 32492
eval/location_props: always produce YXML markup, independent of print_mode;
2009-09-02 reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
wenzelm [Wed, 02 Sep 2009 16:25:44 +0200] rev 32491
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
2009-09-02 tuned ML message;
wenzelm [Wed, 02 Sep 2009 14:11:45 +0200] rev 32490
tuned ML message;
2009-09-02 added "using" to blacklist
nipkow [Wed, 02 Sep 2009 12:20:17 +0200] rev 32489
added "using" to blacklist
2009-09-02 merged
wenzelm [Wed, 02 Sep 2009 10:54:52 +0200] rev 32488
merged
2009-09-02 merged
wenzelm [Wed, 02 Sep 2009 10:35:47 +0200] rev 32487
merged
2009-09-01 removed old Isar document model;
wenzelm [Tue, 01 Sep 2009 21:40:10 +0200] rev 32486
removed old Isar document model;
2009-09-01 corrected spelling
haftmann [Tue, 01 Sep 2009 21:46:38 +0200] rev 32485
corrected spelling
2009-09-01 merged
haftmann [Tue, 01 Sep 2009 21:44:19 +0200] rev 32484
merged
2009-09-01 added -q switch for run in qnd mode
haftmann [Tue, 01 Sep 2009 17:02:09 +0200] rev 32483
added -q switch for run in qnd mode
2009-09-01 code generator is now a separate component
haftmann [Tue, 01 Sep 2009 16:39:05 +0200] rev 32482
code generator is now a separate component
2009-09-01 tuned document
haftmann [Tue, 01 Sep 2009 16:00:59 +0200] rev 32481
tuned document
2009-09-01 some reorganization of number theory
haftmann [Tue, 01 Sep 2009 16:00:57 +0200] rev 32480
some reorganization of number theory
2009-09-01 some reorganization of number theory
haftmann [Tue, 01 Sep 2009 15:39:33 +0200] rev 32479
some reorganization of number theory
2009-09-01 merged
haftmann [Tue, 01 Sep 2009 14:13:34 +0200] rev 32478
merged
2009-09-01 tuned
haftmann [Tue, 01 Sep 2009 14:12:18 +0200] rev 32477
tuned
2009-08-24 avoid long line
haftmann [Mon, 24 Aug 2009 08:31:41 +0200] rev 32476
avoid long line
2009-09-01 added txt to blacklist
nipkow [Tue, 01 Sep 2009 19:48:11 +0200] rev 32475
added txt to blacklist
2009-09-01 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm [Tue, 01 Sep 2009 21:03:04 +0200] rev 32474
Isabelle_Process: receiver as Actor, not EventBus; removed misleading Isabelle_Process.parse_message method -- use plain function instead;
2009-09-01 merged
boehmes [Tue, 01 Sep 2009 15:21:22 +0200] rev 32473
merged
2009-09-01 Mirabelle: actions are responsible for their log messages, output is better readable
boehmes [Tue, 01 Sep 2009 15:20:21 +0200] rev 32472
Mirabelle: actions are responsible for their log messages, output is better readable
2009-09-01 merged
wenzelm [Tue, 01 Sep 2009 14:57:03 +0200] rev 32471
merged
2009-09-01 merged
boehmes [Tue, 01 Sep 2009 14:10:38 +0200] rev 32470
merged
2009-09-01 Mirabelle: added preliminary documentation,
boehmes [Tue, 01 Sep 2009 14:09:59 +0200] rev 32469
Mirabelle: added preliminary documentation, Mirabelle: removed option "verbose", Mirabelle: actions need to limit their execution time themselves, sledgehammer: do not report chained facts
2009-08-31 Mirabelle: explicit command blacklist, preliminary documentation
boehmes [Mon, 31 Aug 2009 19:28:37 +0200] rev 32468
Mirabelle: explicit command blacklist, preliminary documentation
2009-09-01 modernized Isar_Document;
wenzelm [Tue, 01 Sep 2009 14:51:40 +0200] rev 32467
modernized Isar_Document;
2009-09-01 modernized Thy_Header;
wenzelm [Tue, 01 Sep 2009 14:45:06 +0200] rev 32466
modernized Thy_Header;
2009-09-01 misc cleanup and internal reorganization;
wenzelm [Tue, 01 Sep 2009 13:31:22 +0200] rev 32465
misc cleanup and internal reorganization;
2009-09-01 added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
wenzelm [Tue, 01 Sep 2009 11:52:19 +0200] rev 32464
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
2009-08-31 moved lemma Wellfounded.in_inv_image to Relation.thy
krauss [Mon, 31 Aug 2009 20:34:48 +0200] rev 32463
moved lemma Wellfounded.in_inv_image to Relation.thy
2009-08-31 moved wfrec to Recdef.thy
krauss [Mon, 31 Aug 2009 20:34:44 +0200] rev 32462
moved wfrec to Recdef.thy
2009-08-31 no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
krauss [Mon, 31 Aug 2009 20:32:00 +0200] rev 32461
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
2009-08-31 Mirabelle: handle possible parser exceptions, emit suitable log message
boehmes [Mon, 31 Aug 2009 17:32:29 +0200] rev 32460
Mirabelle: handle possible parser exceptions, emit suitable log message
2009-08-31 merged
boehmes [Mon, 31 Aug 2009 15:30:11 +0200] rev 32459
merged
2009-08-31 sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes [Mon, 31 Aug 2009 15:29:26 +0200] rev 32458
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
2009-08-31 merged
nipkow [Mon, 31 Aug 2009 14:10:11 +0200] rev 32457
merged
2009-08-31 tuned the simp rules for Int involving insert and intervals.
nipkow [Mon, 31 Aug 2009 14:09:42 +0200] rev 32456
tuned the simp rules for Int involving insert and intervals.
2009-08-31 Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
boehmes [Mon, 31 Aug 2009 12:22:15 +0200] rev 32455
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
2009-08-31 Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes [Mon, 31 Aug 2009 09:28:50 +0200] rev 32454
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
2009-08-29 merged
boehmes [Sat, 29 Aug 2009 22:01:55 +0200] rev 32453
merged
2009-08-29 apply metis with found theorems in case sledgehammer was successful
boehmes [Sat, 29 Aug 2009 21:58:33 +0200] rev 32452
apply metis with found theorems in case sledgehammer was successful
2009-08-29 propagate theorem names, in addition to generated return message
boehmes [Sat, 29 Aug 2009 21:57:06 +0200] rev 32451
propagate theorem names, in addition to generated return message
2009-08-29 misc tuning;
wenzelm [Sat, 29 Aug 2009 14:31:39 +0200] rev 32450
misc tuning;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip