tuned code setup

code generator more liberal with respect to sort constraints of instance parameters

more Isar for example

tuned funpow code generation

tuned min/max code generation

dropped superfluous if

tuned of_nat code generation

re-introduces axiom subst

corrected SML undefined

updated to official version as of 07-Oct-2008;

fold_lines: more tuning, avoiding extra split_last;

extra check of PROOFGENERAL_HOME;

needs -b option for isabelle getenv

updated generated file;

tuned isabelle usage;

updated generated file;

simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;

updated generated file;

replaced ISABELLE by ISABELLE_PROCESS;

ISABELLE_PROCESS commandline;

replaced ISATOOL by ISABELLE_TOOL;

ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL -- old bindings stay for a while (legacy feature);

eliminated prompt messages;

added isabelle_tool version as basic integrity check of platform/distribution;

renamed isatool to isabelle_tool in programming interfaces;

Theory header keywords.

added Thy/thy_header.scala;

tuned quotes;

factor: proper padding of digits;

plain process_id function;

removed obsolete Posix/Signal compatibility wrappers;

removed obsolete Posix/Signal compatibility wrappers; plain process_id function; adapted to recent changes in Pure;

removed obsolete Posix/Signal compatibility wrappers; plain process_id function;

do not handle Error (which matches arbitrary exceptions!), but ERROR _;

updated to new AtpManager;

operate on Proof.state, not Toplevel.state; moved setup to ATP_Linkup.thy;

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';

perform atp_setups here;

updated generated file;

removed HOL-Plain -- already included in HOL;

removed spurious ResAtp.set_prover;

simplified thread creation via SimpleThread;

simplified thread creation via SimpleThread; managing_thread: option type (fork of inactive thread assumes threads are available in the first place);

version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler);

removed old/unused setup of raw ATP oracles;

tuned;

Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);

added PROOFGENERAL_EMACS, with attempt to find Carbon Emacs;

tuned tracing;

slower heartbeat;

added simple heartbeat thread;

time factor: one more digit;

more tuning of tracing messages;

include factor in timing report;

with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition; removed pointless comments;

tracing: ignore failure of any kind;

tuned SYNCHRONIZED: outermost Exn.release; tuned tracing;

program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;

added partiality section

corrected class antiquotation

max_threads_value always 1 for dummy version;

simplified Exn.EXCEPTIONS, flatten nested occurrences;

simplified Exn.EXCEPTIONS;

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;

tuned

Yet another proof of Newman's lemma, this time using the coherent logic prover.

unit_source: more rigid parsing, stop after final qed;

excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context; tuned;

replaced can_defer by is_relevant (negation); future_proof: declare forked goal to prevent accidental generalization (e.g. instance goal);

datatype transition: internal trans field is maintained in reverse order; tuned;

future_proof: protect conclusion of deferred proof state;

future_schedule: back to one group for all loader tasks;

tuned comments;

fixed

renamed promise to future, tuned related interfaces;

more robust treatment of Interrupt (cf. exn.ML); future_schedule: group each theory separately;

more robust treatment of Interrupt; added release_all, release_first; proper signature;

more robust treatment of Interrupt (cf. exn.ML);

removed release_results (cf. Exn.release_all, Exn.release_first);

more precise join_futures, improved termination;

added more_antiquote.ML

extract Isabelle dist name correctly

unit_source: explicit treatment of 'oops' proofs;

promise_proof: proper statement with empty vars;

load_thy: more precise treatment of improper cmd or proof (notably 'oops');

schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);

added unit_source: commands with proof;

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;

load_thy: Toplevel.excursion based on units of command/proof pairs;

more command categories; tuned;

renamed Future.fork_irrelevant to Future.fork_background; tuned;

export explicit joint_futures, removed Theory.at_end hook; renamed Future.fork_irrelevant to Future.fork_background;

tuned

turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);

Toplevel.commit_exit: position;

export setmp_thread_position; commit_exit: position; added plain command execution; simplified command_excursion, eliminated old (present_)excursion;