wenzelm [Fri, 03 Oct 2008 21:13:17 +0200] rev 28492
factor: proper padding of digits;
wenzelm [Fri, 03 Oct 2008 21:06:39 +0200] rev 28491
plain process_id function;
wenzelm [Fri, 03 Oct 2008 21:06:38 +0200] rev 28490
removed obsolete Posix/Signal compatibility wrappers;
wenzelm [Fri, 03 Oct 2008 21:06:37 +0200] rev 28489
removed obsolete Posix/Signal compatibility wrappers;
plain process_id function;
adapted to recent changes in Pure;
wenzelm [Fri, 03 Oct 2008 21:06:36 +0200] rev 28488
removed obsolete Posix/Signal compatibility wrappers;
plain process_id function;
wenzelm [Fri, 03 Oct 2008 20:10:44 +0200] rev 28487
do not handle Error (which matches arbitrary exceptions!), but ERROR _;
wenzelm [Fri, 03 Oct 2008 20:10:43 +0200] rev 28486
updated to new AtpManager;
wenzelm [Fri, 03 Oct 2008 19:35:18 +0200] rev 28485
operate on Proof.state, not Toplevel.state;
moved setup to ATP_Linkup.thy;
wenzelm [Fri, 03 Oct 2008 19:35:17 +0200] rev 28484
misc simplifcation and tuning;
no export of structure Provers;
added add_provers, print_provers;
operate on Proof.state, not Toplevel.state;
use Time.+ etc. to make SML/XL of NJ happy;
explicit Isar commands 'atp_kill', 'atp_info', 'print_atps';
wenzelm [Fri, 03 Oct 2008 19:35:16 +0200] rev 28483
perform atp_setups here;
wenzelm [Fri, 03 Oct 2008 19:35:15 +0200] rev 28482
updated generated file;
wenzelm [Fri, 03 Oct 2008 19:35:14 +0200] rev 28481
removed HOL-Plain -- already included in HOL;
wenzelm [Fri, 03 Oct 2008 19:17:37 +0200] rev 28480
removed spurious ResAtp.set_prover;
wenzelm [Fri, 03 Oct 2008 17:07:41 +0200] rev 28479
simplified thread creation via SimpleThread;
wenzelm [Fri, 03 Oct 2008 17:07:39 +0200] rev 28478
simplified thread creation via SimpleThread;
managing_thread: option type (fork of inactive thread assumes threads are available in the first place);
wenzelm [Fri, 03 Oct 2008 16:37:09 +0200] rev 28477
version of sledgehammer using threads instead of processes, misc cleanup;
(by Fabian Immler);
wenzelm [Fri, 03 Oct 2008 15:20:33 +0200] rev 28476
removed old/unused setup of raw ATP oracles;
wenzelm [Fri, 03 Oct 2008 14:07:41 +0200] rev 28475
tuned;
wenzelm [Fri, 03 Oct 2008 14:06:19 +0200] rev 28474
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm [Fri, 03 Oct 2008 13:21:01 +0200] rev 28473
added PROOFGENERAL_EMACS, with attempt to find Carbon Emacs;
wenzelm [Fri, 03 Oct 2008 00:21:48 +0200] rev 28472
tuned tracing;
wenzelm [Fri, 03 Oct 2008 00:12:13 +0200] rev 28471
slower heartbeat;
wenzelm [Thu, 02 Oct 2008 23:52:12 +0200] rev 28470
added simple heartbeat thread;
wenzelm [Thu, 02 Oct 2008 23:52:10 +0200] rev 28469
time factor: one more digit;
wenzelm [Thu, 02 Oct 2008 23:30:44 +0200] rev 28468
more tuning of tracing messages;
wenzelm [Thu, 02 Oct 2008 22:09:22 +0200] rev 28467
include factor in timing report;
wenzelm [Thu, 02 Oct 2008 21:21:21 +0200] rev 28466
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
removed pointless comments;
wenzelm [Thu, 02 Oct 2008 19:59:01 +0200] rev 28465
tracing: ignore failure of any kind;
wenzelm [Thu, 02 Oct 2008 19:59:00 +0200] rev 28464
tuned SYNCHRONIZED: outermost Exn.release;
tuned tracing;
wenzelm [Thu, 02 Oct 2008 19:38:48 +0200] rev 28463
program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;
haftmann [Thu, 02 Oct 2008 17:18:36 +0200] rev 28462
added partiality section
haftmann [Thu, 02 Oct 2008 17:18:22 +0200] rev 28461
corrected class antiquotation
wenzelm [Thu, 02 Oct 2008 14:22:45 +0200] rev 28460
max_threads_value always 1 for dummy version;
wenzelm [Thu, 02 Oct 2008 14:22:44 +0200] rev 28459
simplified Exn.EXCEPTIONS, flatten nested occurrences;
wenzelm [Thu, 02 Oct 2008 14:22:40 +0200] rev 28458
simplified Exn.EXCEPTIONS;
wenzelm [Thu, 02 Oct 2008 14:22:36 +0200] rev 28457
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
haftmann [Thu, 02 Oct 2008 13:07:33 +0200] rev 28456
tuned
berghofe [Thu, 02 Oct 2008 12:17:20 +0200] rev 28455
Yet another proof of Newman's lemma, this time using the coherent logic prover.
wenzelm [Wed, 01 Oct 2008 22:33:29 +0200] rev 28454
unit_source: more rigid parsing, stop after final qed;
wenzelm [Wed, 01 Oct 2008 22:33:28 +0200] rev 28453
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
tuned;
wenzelm [Wed, 01 Oct 2008 22:33:24 +0200] rev 28452
replaced can_defer by is_relevant (negation);
future_proof: declare forked goal to prevent accidental generalization (e.g. instance goal);
wenzelm [Wed, 01 Oct 2008 20:02:37 +0200] rev 28451
datatype transition: internal trans field is maintained in reverse order;
tuned;
wenzelm [Wed, 01 Oct 2008 18:16:14 +0200] rev 28450
future_proof: protect conclusion of deferred proof state;
wenzelm [Wed, 01 Oct 2008 18:16:10 +0200] rev 28449
future_schedule: back to one group for all loader tasks;
wenzelm [Wed, 01 Oct 2008 14:17:06 +0200] rev 28448
tuned comments;
haftmann [Wed, 01 Oct 2008 13:33:54 +0200] rev 28447
fixed
wenzelm [Wed, 01 Oct 2008 12:18:18 +0200] rev 28446
renamed promise to future, tuned related interfaces;
wenzelm [Wed, 01 Oct 2008 12:00:05 +0200] rev 28445
more robust treatment of Interrupt (cf. exn.ML);
future_schedule: group each theory separately;
wenzelm [Wed, 01 Oct 2008 12:00:04 +0200] rev 28444
more robust treatment of Interrupt;
added release_all, release_first;
proper signature;
wenzelm [Wed, 01 Oct 2008 12:00:02 +0200] rev 28443
more robust treatment of Interrupt (cf. exn.ML);
wenzelm [Wed, 01 Oct 2008 12:00:01 +0200] rev 28442
removed release_results (cf. Exn.release_all, Exn.release_first);
wenzelm [Wed, 01 Oct 2008 12:00:00 +0200] rev 28441
more precise join_futures, improved termination;
haftmann [Wed, 01 Oct 2008 08:42:42 +0200] rev 28440
added more_antiquote.ML
kleing [Wed, 01 Oct 2008 00:09:51 +0200] rev 28439
extract Isabelle dist name correctly
wenzelm [Tue, 30 Sep 2008 23:31:40 +0200] rev 28438
unit_source: explicit treatment of 'oops' proofs;
wenzelm [Tue, 30 Sep 2008 23:31:38 +0200] rev 28437
promise_proof: proper statement with empty vars;
wenzelm [Tue, 30 Sep 2008 23:31:36 +0200] rev 28436
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
wenzelm [Tue, 30 Sep 2008 22:02:55 +0200] rev 28435
schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);
wenzelm [Tue, 30 Sep 2008 22:02:53 +0200] rev 28434
added unit_source: commands with proof;
wenzelm [Tue, 30 Sep 2008 22:02:51 +0200] rev 28433
begin_proof: avoid race condition wrt. skip_proofs flag;
replaced command_excursion by excursion, which is based on units of command/proof pairs;
excursion: basic support for proof promises;
wenzelm [Tue, 30 Sep 2008 22:02:50 +0200] rev 28432
load_thy: Toplevel.excursion based on units of command/proof pairs;
wenzelm [Tue, 30 Sep 2008 22:02:47 +0200] rev 28431
more command categories;
tuned;
wenzelm [Tue, 30 Sep 2008 22:02:45 +0200] rev 28430
renamed Future.fork_irrelevant to Future.fork_background;
tuned;
wenzelm [Tue, 30 Sep 2008 22:02:44 +0200] rev 28429
export explicit joint_futures, removed Theory.at_end hook;
renamed Future.fork_irrelevant to Future.fork_background;
haftmann [Tue, 30 Sep 2008 14:30:44 +0200] rev 28428
tuned
wenzelm [Tue, 30 Sep 2008 14:19:28 +0200] rev 28427
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm [Tue, 30 Sep 2008 14:19:27 +0200] rev 28426
Toplevel.commit_exit: position;
wenzelm [Tue, 30 Sep 2008 14:19:26 +0200] rev 28425
export setmp_thread_position;
commit_exit: position;
added plain command execution;
simplified command_excursion, eliminated old (present_)excursion;
wenzelm [Tue, 30 Sep 2008 14:19:25 +0200] rev 28424
simplified process_file, eliminated Toplevel.excursion;
load_thy: separation of Toplevel.command_excursion and ThyOutput.present_thy (intermediate state persist until commit_exit);
haftmann [Tue, 30 Sep 2008 12:49:18 +0200] rev 28423
clarified codegen interfaces
haftmann [Tue, 30 Sep 2008 12:49:17 +0200] rev 28422
tuned
haftmann [Tue, 30 Sep 2008 12:49:16 +0200] rev 28421
reorganized examples
haftmann [Tue, 30 Sep 2008 12:49:14 +0200] rev 28420
fixed slips
haftmann [Tue, 30 Sep 2008 11:19:47 +0200] rev 28419
re-canibalised manual
kleing [Tue, 30 Sep 2008 04:06:55 +0200] rev 28418
slightly different command line for makedist_mercurial
wenzelm [Mon, 29 Sep 2008 21:45:44 +0200] rev 28417
put_thms: ContextPosition.set_visible false;
wenzelm [Mon, 29 Sep 2008 21:26:49 +0200] rev 28416
added type pp, which helps installing polymorphic pretty printers;
wenzelm [Mon, 29 Sep 2008 21:26:46 +0200] rev 28415
added str_of;
wenzelm [Mon, 29 Sep 2008 21:26:44 +0200] rev 28414
install_pp Future.T (polyml only);
wenzelm [Mon, 29 Sep 2008 21:26:41 +0200] rev 28413
report_token/parse_token: back to context-less version;
wenzelm [Mon, 29 Sep 2008 21:26:39 +0200] rev 28412
back to plain Position.report for regular references;
wenzelm [Mon, 29 Sep 2008 21:26:36 +0200] rev 28411
back to plain Position.report for regular references;
ContextPosition.report_visible for decls;
report_token/parse_token: back to context-less version;
wenzelm [Mon, 29 Sep 2008 21:26:32 +0200] rev 28410
promise global proofs;
wenzelm [Mon, 29 Sep 2008 21:26:26 +0200] rev 28409
renamed report to report_visible;
tuned comments;
wenzelm [Mon, 29 Sep 2008 14:59:02 +0200] rev 28408
code example: back to individual ML commands, which are now thread-safe;
wenzelm [Mon, 29 Sep 2008 14:41:25 +0200] rev 28407
ContextPosition.report;
parse_token/report_token: explicit context;
wenzelm [Mon, 29 Sep 2008 14:41:24 +0200] rev 28406
target update: invisible context position avoids duplication of reports etc.;
wenzelm [Mon, 29 Sep 2008 14:41:23 +0200] rev 28405
Context position visibility.
wenzelm [Mon, 29 Sep 2008 14:41:22 +0200] rev 28404
added context_position.ML;
haftmann [Mon, 29 Sep 2008 12:32:00 +0200] rev 28403
more precise redundancy check
haftmann [Mon, 29 Sep 2008 12:31:59 +0200] rev 28402
clarified dependencies between arith tools
haftmann [Mon, 29 Sep 2008 12:31:58 +0200] rev 28401
separate HOL-Main image
haftmann [Mon, 29 Sep 2008 12:31:57 +0200] rev 28400
polished code generator setup
haftmann [Mon, 29 Sep 2008 12:31:56 +0200] rev 28399
added theory antiquotation
wenzelm [Mon, 29 Sep 2008 11:46:52 +0200] rev 28398
tuned comments;
wenzelm [Mon, 29 Sep 2008 11:46:47 +0200] rev 28397
handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm [Mon, 29 Sep 2008 10:58:04 +0200] rev 28396
added norm_export_morphism;
wenzelm [Mon, 29 Sep 2008 10:58:03 +0200] rev 28395
added exit_global, exit_result, exit_result_global;
ProofContext.norm_export_morphism;
wenzelm [Mon, 29 Sep 2008 10:58:01 +0200] rev 28394
LocalTheory.exit_global;
wenzelm [Sun, 28 Sep 2008 14:46:51 +0200] rev 28393
HOL no longer depends on HOL-Plain;
wenzelm [Sun, 28 Sep 2008 14:40:43 +0200] rev 28392
setmp_noncritical;
wenzelm [Sun, 28 Sep 2008 12:42:35 +0200] rev 28391
join earlier promises first;
wenzelm [Sun, 28 Sep 2008 12:23:45 +0200] rev 28390
proper setmp_thread_data for nested execute (cf. join_loop);
wenzelm [Sun, 28 Sep 2008 12:23:44 +0200] rev 28389
promise_result: enforce strictly sequential dependencies, via serial numbers;
kleing [Sun, 28 Sep 2008 09:25:24 +0200] rev 28388
do not cvs update for doc test (switching to mercurial, update done outside
once and for all)
kleing [Sun, 28 Sep 2008 09:13:46 +0200] rev 28387
use mercurial repository for isatest
wenzelm [Sun, 28 Sep 2008 00:00:55 +0200] rev 28386
thread_data: include thread name, export access;
more tracing;
wenzelm [Sat, 27 Sep 2008 19:35:00 +0200] rev 28385
setmp_noncritical;
wenzelm [Sat, 27 Sep 2008 18:18:08 +0200] rev 28384
dequeue_towards: return bound for unfinished tasks;
wenzelm [Sat, 27 Sep 2008 18:18:07 +0200] rev 28383
moved release_results to future.ML;
get_some: simplified via Future.release_results;
wenzelm [Sat, 27 Sep 2008 18:18:06 +0200] rev 28382
added release_results (formerly in par_list.ML);
more informative trace_active;
join_results: avoid deadlock via nested SYNCHRONOIZED, more robust active join, less rechecking of tasks;
wenzelm [Sat, 27 Sep 2008 18:18:05 +0200] rev 28381
Future.release_results;
wenzelm [Sat, 27 Sep 2008 15:37:01 +0200] rev 28380
more tracing;
wenzelm [Sat, 27 Sep 2008 15:20:39 +0200] rev 28379
Theory.checkpoint for main operations, admits concurrent proofs;
wenzelm [Sat, 27 Sep 2008 15:20:37 +0200] rev 28378
promise: include check into future body, i.e. joined results are always valid;
pending future derivations: shared ref within whole theory body, i.e. end-of-theory joins *all* derivations ever forked from a version of the theory;
simplified rep_deriv;
wenzelm [Sat, 27 Sep 2008 15:20:36 +0200] rev 28377
proper transfer of theorems that involve classes being instantiated here;
wenzelm [Sat, 27 Sep 2008 14:26:06 +0200] rev 28376
HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
wenzelm [Fri, 26 Sep 2008 19:07:56 +0200] rev 28375
eliminated polymorphic equality;
wenzelm [Fri, 26 Sep 2008 17:24:15 +0200] rev 28374
added subset operation;
berghofe [Fri, 26 Sep 2008 14:53:10 +0200] rev 28373
Added fresh_star_const.