2008-10-04 wenzelm 2008-10-04 updated generated file;
2008-10-04 wenzelm 2008-10-04 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
2008-10-04 wenzelm 2008-10-04 updated generated file;
2008-10-04 wenzelm 2008-10-04 replaced ISABELLE by ISABELLE_PROCESS;
2008-10-04 wenzelm 2008-10-04 ISABELLE_PROCESS commandline;
2008-10-04 wenzelm 2008-10-04 replaced ISATOOL by ISABELLE_TOOL;
2008-10-04 wenzelm 2008-10-04 ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL -- old bindings stay for a while (legacy feature);
2008-10-04 wenzelm 2008-10-04 eliminated prompt messages;
2008-10-04 wenzelm 2008-10-04 added isabelle_tool version as basic integrity check of platform/distribution;
2008-10-04 wenzelm 2008-10-04 renamed isatool to isabelle_tool in programming interfaces;
2008-10-04 wenzelm 2008-10-04 Theory header keywords.
2008-10-04 wenzelm 2008-10-04 added Thy/thy_header.scala;
2008-10-03 wenzelm 2008-10-03 tuned quotes;
2008-10-03 wenzelm 2008-10-03 factor: proper padding of digits;
2008-10-03 wenzelm 2008-10-03 plain process_id function;
2008-10-03 wenzelm 2008-10-03 removed obsolete Posix/Signal compatibility wrappers;
2008-10-03 wenzelm 2008-10-03 removed obsolete Posix/Signal compatibility wrappers; plain process_id function; adapted to recent changes in Pure;
2008-10-03 wenzelm 2008-10-03 removed obsolete Posix/Signal compatibility wrappers; plain process_id function;
2008-10-03 wenzelm 2008-10-03 do not handle Error (which matches arbitrary exceptions!), but ERROR _;
2008-10-03 wenzelm 2008-10-03 updated to new AtpManager;
2008-10-03 wenzelm 2008-10-03 operate on Proof.state, not Toplevel.state; moved setup to ATP_Linkup.thy;
2008-10-03 wenzelm 2008-10-03 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';
2008-10-03 wenzelm 2008-10-03 perform atp_setups here;
2008-10-03 wenzelm 2008-10-03 updated generated file;
2008-10-03 wenzelm 2008-10-03 removed HOL-Plain -- already included in HOL;
2008-10-03 wenzelm 2008-10-03 removed spurious ResAtp.set_prover;
2008-10-03 wenzelm 2008-10-03 simplified thread creation via SimpleThread;
2008-10-03 wenzelm 2008-10-03 simplified thread creation via SimpleThread; managing_thread: option type (fork of inactive thread assumes threads are available in the first place);
2008-10-03 wenzelm 2008-10-03 version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler);
2008-10-03 wenzelm 2008-10-03 removed old/unused setup of raw ATP oracles;
2008-10-03 wenzelm 2008-10-03 tuned;
2008-10-03 wenzelm 2008-10-03 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
2008-10-03 wenzelm 2008-10-03 added PROOFGENERAL_EMACS, with attempt to find Carbon Emacs;
2008-10-03 wenzelm 2008-10-03 tuned tracing;
2008-10-03 wenzelm 2008-10-03 slower heartbeat;
2008-10-02 wenzelm 2008-10-02 added simple heartbeat thread;
2008-10-02 wenzelm 2008-10-02 time factor: one more digit;
2008-10-02 wenzelm 2008-10-02 more tuning of tracing messages;
2008-10-02 wenzelm 2008-10-02 include factor in timing report;
2008-10-02 wenzelm 2008-10-02 with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition; removed pointless comments;
2008-10-02 wenzelm 2008-10-02 tracing: ignore failure of any kind;
2008-10-02 wenzelm 2008-10-02 tuned SYNCHRONIZED: outermost Exn.release; tuned tracing;
2008-10-02 wenzelm 2008-10-02 program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;
2008-10-02 haftmann 2008-10-02 added partiality section
2008-10-02 haftmann 2008-10-02 corrected class antiquotation
2008-10-02 wenzelm 2008-10-02 max_threads_value always 1 for dummy version;
2008-10-02 wenzelm 2008-10-02 simplified Exn.EXCEPTIONS, flatten nested occurrences;
2008-10-02 wenzelm 2008-10-02 simplified Exn.EXCEPTIONS;
2008-10-02 wenzelm 2008-10-02 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;
2008-10-02 haftmann 2008-10-02 tuned
2008-10-02 berghofe 2008-10-02 Yet another proof of Newman's lemma, this time using the coherent logic prover.
2008-10-01 wenzelm 2008-10-01 unit_source: more rigid parsing, stop after final qed;
2008-10-01 wenzelm 2008-10-01 excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context; tuned;
2008-10-01 wenzelm 2008-10-01 replaced can_defer by is_relevant (negation); future_proof: declare forked goal to prevent accidental generalization (e.g. instance goal);
2008-10-01 wenzelm 2008-10-01 datatype transition: internal trans field is maintained in reverse order; tuned;
2008-10-01 wenzelm 2008-10-01 future_proof: protect conclusion of deferred proof state;
2008-10-01 wenzelm 2008-10-01 future_schedule: back to one group for all loader tasks;
2008-10-01 wenzelm 2008-10-01 tuned comments;
2008-10-01 haftmann 2008-10-01 fixed
2008-10-01 wenzelm 2008-10-01 renamed promise to future, tuned related interfaces;