haftmann [Fri, 18 Sep 2009 09:07:48 +0200] rev 32601
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann [Fri, 18 Sep 2009 07:54:26 +0200] rev 32600
tuned NEWS, added CONTRIBUTORS
nipkow [Thu, 17 Sep 2009 19:13:22 +0200] rev 32599
merged
nipkow [Thu, 17 Sep 2009 19:13:07 +0200] rev 32598
removed misleading log line
paulson [Thu, 17 Sep 2009 15:04:46 +0100] rev 32597
NEWS: New method metisFT
paulson [Thu, 17 Sep 2009 14:59:58 +0100] rev 32596
New theorems for proving equalities and inclusions involving unions
boehmes [Thu, 17 Sep 2009 14:07:44 +0200] rev 32595
added time limit for extraction phase (not supported on Cygwin)
boehmes [Thu, 17 Sep 2009 11:58:21 +0200] rev 32594
merged
boehmes [Thu, 17 Sep 2009 11:57:36 +0200] rev 32593
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
new "eproof" script written in Perl (hopefully more stable than the one coming with E)
wenzelm [Wed, 16 Sep 2009 22:46:10 +0200] rev 32592
Synchronized.value does not require locking, since assigments are atomic;
removed obsolete Synchronized.peek;
wenzelm [Wed, 16 Sep 2009 21:31:57 +0200] rev 32591
tuned;
wenzelm [Wed, 16 Sep 2009 21:14:08 +0200] rev 32590
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
haftmann [Wed, 16 Sep 2009 13:43:15 +0200] rev 32589
merged
haftmann [Wed, 16 Sep 2009 13:43:07 +0200] rev 32588
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann [Wed, 16 Sep 2009 13:43:05 +0200] rev 32587
Inter and Union are mere abbreviations for Inf and Sup
nipkow [Wed, 16 Sep 2009 13:03:03 +0200] rev 32586
merged
nipkow [Wed, 16 Sep 2009 12:47:14 +0200] rev 32585
revised lemma counting
haftmann [Wed, 16 Sep 2009 09:04:41 +0200] rev 32584
merged
haftmann [Tue, 15 Sep 2009 19:16:47 +0200] rev 32583
merged
haftmann [Tue, 15 Sep 2009 19:16:35 +0200] rev 32582
hide new constants
haftmann [Tue, 15 Sep 2009 15:41:30 +0200] rev 32581
merged
haftmann [Tue, 15 Sep 2009 15:41:23 +0200] rev 32580
restored code generation for OCaml
haftmann [Tue, 15 Sep 2009 15:22:15 +0200] rev 32579
added singleton example
haftmann [Tue, 15 Sep 2009 12:11:10 +0200] rev 32578
added emptiness check predicate and singleton projection
wenzelm [Wed, 16 Sep 2009 00:12:52 +0200] rev 32577
added append_after (tuned version of former insert_after of Seq);
wenzelm [Tue, 15 Sep 2009 23:57:07 +0200] rev 32576
double linking for improved performance of "prev";
misc tuning;
wenzelm [Tue, 15 Sep 2009 15:44:57 +0200] rev 32575
merged
boehmes [Tue, 15 Sep 2009 15:29:11 +0200] rev 32574
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
separate Perl script to invoke local ATPs and measure their user time, with proper setup of process groups required by E
wenzelm [Tue, 15 Sep 2009 15:17:53 +0200] rev 32573
Isar.define_command: identify transaction;
wenzelm [Tue, 15 Sep 2009 13:09:13 +0200] rev 32572
updated bib;
nipkow [Mon, 14 Sep 2009 19:30:48 +0200] rev 32571
count number of iterations required for minimization (and fixed bug: minimization was always called)
haftmann [Mon, 14 Sep 2009 12:25:02 +0200] rev 32570
merged
haftmann [Mon, 14 Sep 2009 08:36:58 +0200] rev 32569
more antiquotations
haftmann [Mon, 14 Sep 2009 08:36:57 +0200] rev 32568
some lemmas about strict order in lattices
wenzelm [Sun, 13 Sep 2009 02:10:41 +0200] rev 32567
explicitly export type abbreviations (as usual in SML97);
explicit type constraints for record patterns -- SML does not support record polymorphism;
observe max. line length (80-100);
wenzelm [Sun, 13 Sep 2009 02:07:52 +0200] rev 32566
wrapper for Real.fmt -- via StringCvt.realfmt;
wenzelm [Sun, 13 Sep 2009 02:07:06 +0200] rev 32565
made SML/NJ happy;
wenzelm [Sat, 12 Sep 2009 16:30:48 +0200] rev 32564
standard headers and text sections;
nipkow [Fri, 11 Sep 2009 09:53:02 +0200] rev 32563
merged
nipkow [Fri, 11 Sep 2009 09:52:40 +0200] rev 32562
Made record parameter flexible to allow for extensions
haftmann [Fri, 11 Sep 2009 09:05:26 +0200] rev 32561
merged
haftmann [Fri, 11 Sep 2009 09:04:51 +0200] rev 32560
corrected upper/lowercase
haftmann [Thu, 10 Sep 2009 17:14:05 +0200] rev 32559
merged
haftmann [Thu, 10 Sep 2009 15:26:51 +0200] rev 32558
obey underscore naming convention
haftmann [Thu, 10 Sep 2009 15:23:09 +0200] rev 32557
plain structure name; signature constraint; shorter lines
haftmann [Thu, 10 Sep 2009 15:23:08 +0200] rev 32556
split of test examples from NatTransfer
haftmann [Thu, 10 Sep 2009 15:23:08 +0200] rev 32555
generic transfer procedure
haftmann [Thu, 10 Sep 2009 15:23:07 +0200] rev 32554
early bootstrap of generic transfer procedure
haftmann [Thu, 10 Sep 2009 14:07:58 +0200] rev 32553
cleanedup theorems all_nat ex_nat
Philipp Meyer [Thu, 10 Sep 2009 16:16:18 +0200] rev 32552
atp_minimize is now not using whitelist
nipkow [Thu, 10 Sep 2009 15:57:55 +0200] rev 32551
position information is now passed to all actions;
mirabele_s/h logs all proved positions.
nipkow [Thu, 10 Sep 2009 12:53:49 +0200] rev 32550
logging number of metis lemmas
nipkow [Wed, 09 Sep 2009 23:26:34 +0200] rev 32549
minimization: comparing w/ and w/o.
haftmann [Wed, 09 Sep 2009 12:29:06 +0200] rev 32548
merged
haftmann [Wed, 09 Sep 2009 12:24:22 +0200] rev 32547
dropped accidental code additions
haftmann [Wed, 09 Sep 2009 12:27:41 +0200] rev 32546
merged
haftmann [Wed, 09 Sep 2009 12:27:12 +0200] rev 32545
explicit transfer avoids spurious merge problems
haftmann [Wed, 09 Sep 2009 11:31:20 +0200] rev 32544
moved eq handling in nbe into separate oracle
wenzelm [Tue, 08 Sep 2009 18:31:26 +0200] rev 32543
tuned document -- proper text instead of source comments, reduced line length;
Philipp Meyer [Tue, 01 Sep 2009 11:19:49 +0200] rev 32542
fixed cleanup routine in neos csdp script
boehmes [Tue, 08 Sep 2009 09:57:33 +0200] rev 32541
timeout option for ATPs
wenzelm [Mon, 07 Sep 2009 22:13:32 +0200] rev 32540
merged
wenzelm [Mon, 07 Sep 2009 22:12:16 +0200] rev 32539
modernized Event_Bus -- based on actors;
nipkow [Mon, 07 Sep 2009 22:08:05 +0200] rev 32538
Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)
nipkow [Mon, 07 Sep 2009 19:41:30 +0200] rev 32537
merged
nipkow [Mon, 07 Sep 2009 19:41:07 +0200] rev 32536
tuned stats
paulson [Mon, 07 Sep 2009 17:02:15 +0100] rev 32535
Fixed a few problems with the method metisFT
nipkow [Mon, 07 Sep 2009 16:25:12 +0200] rev 32534
merged
nipkow [Mon, 07 Sep 2009 16:24:32 +0200] rev 32533
tuned stats
paulson [Mon, 07 Sep 2009 13:19:09 +0100] rev 32532
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson [Mon, 07 Sep 2009 11:44:12 +0100] rev 32531
merged
paulson [Mon, 07 Sep 2009 10:04:17 +0100] rev 32530
conflict resolution possibly
paulson [Fri, 04 Sep 2009 11:37:24 +0100] rev 32529
New method, metisFT: a fully-typed proof search that should eliminate type errors during reconstruction
paulson [Fri, 28 Aug 2009 13:32:20 +0100] rev 32528
merged
paulson [Thu, 27 Aug 2009 15:49:45 +0100] rev 32527
More streamlining using metis.
nipkow [Mon, 07 Sep 2009 08:32:22 +0200] rev 32526
enabled metis permanently, tuned stats
boehmes [Sat, 05 Sep 2009 22:01:31 +0200] rev 32525
added signature ATP_MINIMAL,
fixed AtpMinimal.minimalize for the trivial case,
Mirabelle: added an option to minimize a theorem set found by sledgehammer,
use timeout of sledgehammer instead of additional timeLimit
boehmes [Sat, 05 Sep 2009 17:35:05 +0200] rev 32524
merged
boehmes [Sat, 05 Sep 2009 17:34:30 +0200] rev 32523
separate output of ATP user time and sledgehammer (ML code) user time
boehmes [Sat, 05 Sep 2009 15:46:52 +0200] rev 32522
Mirabelle: command-line action options may either be key=value or just key
boehmes [Sat, 05 Sep 2009 11:45:57 +0200] rev 32521
added initialization and cleanup of actions,
added option to suppress Isabelle output,
sledgehammer action produces its own report (no need for additional perl script)
haftmann [Fri, 04 Sep 2009 15:19:51 +0200] rev 32520
merged
haftmann [Fri, 04 Sep 2009 15:18:35 +0200] rev 32519
tuned metis proofs
boehmes [Fri, 04 Sep 2009 13:57:56 +0200] rev 32518
tuned
nipkow [Fri, 04 Sep 2009 10:58:50 +0200] rev 32517
tuned output
boehmes [Thu, 03 Sep 2009 22:48:18 +0200] rev 32516
merged
boehmes [Thu, 03 Sep 2009 22:47:31 +0200] rev 32515
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
removed PolyML.makestring (no strict dependency on PolyML anymore)
haftmann [Thu, 03 Sep 2009 20:26:07 +0200] rev 32514
merged
haftmann [Thu, 03 Sep 2009 17:26:10 +0200] rev 32513
merged
haftmann [Thu, 03 Sep 2009 15:39:02 +0200] rev 32512
proper class syntax for sublocale class < expr
boehmes [Thu, 03 Sep 2009 18:41:58 +0200] rev 32511
added option full_typed for sledgehammer action
boehmes [Thu, 03 Sep 2009 17:55:31 +0200] rev 32510
added runtime information to sledgehammer
boehmes [Thu, 03 Sep 2009 15:47:39 +0200] rev 32509
tuned
nipkow [Thu, 03 Sep 2009 15:30:05 +0200] rev 32508
scaled avg_time
nipkow [Thu, 03 Sep 2009 14:50:02 +0200] rev 32507
merged
nipkow [Thu, 03 Sep 2009 14:49:34 +0200] rev 32506
tuned
krauss [Thu, 03 Sep 2009 14:40:52 +0200] rev 32505
isatest: collect test results and logs in testdata repository
boehmes [Thu, 03 Sep 2009 14:31:04 +0200] rev 32504
replaced backlist by whitelist
boehmes [Thu, 03 Sep 2009 14:05:13 +0200] rev 32503
Mirabelle: logging of exceptions (works only for PolyML)
wenzelm [Wed, 02 Sep 2009 22:12:40 +0200] rev 32502
merged
wenzelm [Wed, 02 Sep 2009 22:12:20 +0200] rev 32501
refined delay into delay_first/delay_last;
boehmes [Wed, 02 Sep 2009 21:34:13 +0200] rev 32500
merged
boehmes [Wed, 02 Sep 2009 21:33:16 +0200] rev 32499
add report script for Mirabelle
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)
boehmes [Wed, 02 Sep 2009 16:29:50 +0200] rev 32497
removed errors overseen in previous changes
boehmes [Wed, 02 Sep 2009 16:23:53 +0200] rev 32496
moved Mirabelle from HOL/Tools to HOL,
added session HOL-Mirabelle
boehmes [Wed, 02 Sep 2009 16:02:37 +0200] rev 32495
removed unused signature
wenzelm [Wed, 02 Sep 2009 20:49:04 +0200] rev 32494
explicit checks;
wenzelm [Wed, 02 Sep 2009 17:33:25 +0200] rev 32493
updated Poly/ML SVN version;
wenzelm [Wed, 02 Sep 2009 16:51:19 +0200] rev 32492
eval/location_props: always produce YXML markup, independent of print_mode;
wenzelm [Wed, 02 Sep 2009 16:25:44 +0200] rev 32491
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
wenzelm [Wed, 02 Sep 2009 14:11:45 +0200] rev 32490
tuned ML message;
nipkow [Wed, 02 Sep 2009 12:20:17 +0200] rev 32489
added "using" to blacklist
wenzelm [Wed, 02 Sep 2009 10:54:52 +0200] rev 32488
merged
wenzelm [Wed, 02 Sep 2009 10:35:47 +0200] rev 32487
merged
wenzelm [Tue, 01 Sep 2009 21:40:10 +0200] rev 32486
removed old Isar document model;
haftmann [Tue, 01 Sep 2009 21:46:38 +0200] rev 32485
corrected spelling
haftmann [Tue, 01 Sep 2009 21:44:19 +0200] rev 32484
merged
haftmann [Tue, 01 Sep 2009 17:02:09 +0200] rev 32483
added -q switch for run in qnd mode
haftmann [Tue, 01 Sep 2009 16:39:05 +0200] rev 32482
code generator is now a separate component