added Future.enabled check;

ThyOutput: export some auxiliary operations;

fixed proof

added lemmas

Names of variables in perm_eqs are now chosen more carefully to avoid clashes with name "pi".

- removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML) - improved code unfold preprocessor: now uses one single simpset containing all unfolding rules - got rid of some legacy functions

datatype_codegen now checks name of result type of constructor to avoid problems with overloaded constants such as 0.

run a program in a modified environment;

reactivated HOL-Matrix; minor cleanup;

tuned

filled remaining gaps

added type antiquotation

tuned;

added dep for Concurrent/ROOT.ML;

tuned;

removed Locales;

goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;

added translations for SORT_CONSTRAINT tuned;

conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;

added make;

maintain sort occurrences of declared terms;

added weaken_sorts; strip_shyps: minimal list of minimized extra sorts; tuned;

added make, minimal_sorts;

added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;

added check_shyps, which reject pending sort hypotheses;

Drule.norm_hhf_eqs;

prove_common: include all sorts from context into statement, check shyps of result; Drule.norm_hhf_eqs;

added rules for sort_constraint, include in norm_hhf_eqs; tuned;

tuned;

avoid accidental dependency of automated proof on sort equiv;

explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;

avoid CRITICAL with_path;

rewrite more proofs in Isar style

Removed ex/Locales.thy.

More occurrences of 'includes' gone.

Removed outdated locales tutorial.

correct rounding

circumvent some TeX problem

only test HOL image for smlnj

tuned;

tuned;

generic ATP manager based on threads (by Fabian Immler);

added sledgehammer etc.;

removed obsolete Complex sessions;

figure for adaption

Removed 'includes' (fixed).

Removed 'includes'.

give more time to do inital loggin and settings read

log start of test session

tuned interfaces -- plain prover function, without thread; misc tuning and simplification; reduced NJ basis library stuff to bare minimum;

add_prover: plain prover function, without thread; removed obsolete atp_thread interface; moved kill_excessive into main thread manager loop -- avoids race condition wrt. register/unregister; start_prover: register/unregister self -- avoids race condition;

tuned AtpWrapper interfaces;

continued codegen tutorial

renamed AtpThread to AtpWrapper;

adding preferences is now permissive;

tuned;

adding preferences is now permissive, no error handling here; tuned messages;

CRITICAL access to preferences; tuned some interfaces;

export generic_pref etc.; CRITICAL access to preferences; misc cleanup, more conventional indentation;

renamed kill_all to kill, in conformance with atp_kill command; simplified/unified treatment of preferences; check_thread_manager: CRITICAL due to global ref; goal addressing via Thm.cprem_of; reduced NJ basis library stuff to bare minimum;

tuned comments;

added lemma

Added liveness analysis

info: back to plain printing; maintain state as Synchronized.var (cf. Pure/Concurrent/synchronized.ML); turned start into check_thread_manager, which forks the managing thread on demand; simplified heap operations; default preferences: only include e prover, which is most likely to be installed; misc simplifcation and tuning;

added min_elem, upto;

added value; simplified synchronized variable access;

simplified synchronized variable access; tuned;

State variables with synchronized access.

added generic combinator for synchronized evaluation (formerly in future.ML);

simplified implementation using Synchronized.var;

SimpleThread.synchronized;

added Concurrent/synchronized.ML;

** Update from Fabian ** added remote prover functions;

** Update from Fabian ** reset print mode when producing proof text;

** Update from Fabian ** preferences/provers: separated by white space, avoid low-level char type; sledgehammer command accepts prover list as well; avoid I/O in critical section of AtpManager.info; more systematic synchronization using higher-order combinators; more descriptive errors when atp fails; keep explicitly requested problem files; added remote prover functions; simplified treatment of prover name in diagnostic output; misc tuning and cleanup;

tuned output;

tuned

tuned

change DISTPREFIX to not use yet another filesystem

tuned

tuned

tuned

tuned

`code func` now just `code`

some adaption

using tikz pictures

tuned default rules of (dvd)

replaced str_of by general peek;

extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;

fixed spelling;

added enabled; removed pseudo-parallel version of profile -- CRITICAL prevents future join;

added enabled;

Multithreading.enabled;

moved future_scheduler flag to Concurrent/ROOT.ML;

added invalidate_group; SimpleThread.interrupt;

added fail-safe interrupt;

subject to Multithreading.enabled; raw_map: join sequentially, less overhead;

future result: Interrupt invalidates group, but pretends success otherwise;

added future_scheduler flag (tmp!), from skip_proofs.ML; added Concurrent/par_list_dummy.ML;

Dummy version of parallel list combinators -- plain sequential evaluation.

added Concurrent/par_list_dummy.ML;

improved performance of skolem cache, due to parallel map; misc tuning, less verbosity;

SimpleThread.interrupt;

report: back to single message;

added section label;

tuned

do logging to MASTERLOG centrally (avoid multiple writers over NFS as this tends to corrupt the log file if not mounted with -sync option which apparently is not the default any more).

removed legacy |>>>

established canonical argument order in SML code generators

established canonical argument order

made SMLNJ happy

less tracing; removed heartbeat thread;

Future.joint_results is already uninterruptible;

more careful handling of group interrupts; join control is uninterruptible; less tracing;

use polyml-cvs, which fixes a serious deadlock problem of Poly/ML runtime vs. GC;

added HOL-Main;

setmp_noncritical makes it work with future scheduler;

The result of the equality inference rule no longer undergoes factoring.

make the test for experimental sessions in isatest-check actually work (test for log files ending in e.log)

leave a log message when no snapshot is generated

clarified preprocessor policies

arbitrary is undefined

tuned whitespace

only one theorem table for both code generators

proper default codegen attribute

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;

simplified process_file, eliminated Toplevel.excursion; load_thy: separation of Toplevel.command_excursion and ThyOutput.present_thy (intermediate state persist until commit_exit);

clarified codegen interfaces

tuned

reorganized examples

fixed slips

re-canibalised manual

slightly different command line for makedist_mercurial

put_thms: ContextPosition.set_visible false;

added type pp, which helps installing polymorphic pretty printers;

added str_of;

install_pp Future.T (polyml only);

report_token/parse_token: back to context-less version;

back to plain Position.report for regular references;

back to plain Position.report for regular references; ContextPosition.report_visible for decls; report_token/parse_token: back to context-less version;

promise global proofs;

renamed report to report_visible; tuned comments;

code example: back to individual ML commands, which are now thread-safe;

ContextPosition.report; parse_token/report_token: explicit context;

target update: invisible context position avoids duplication of reports etc.;

Context position visibility.

added context_position.ML;

more precise redundancy check

clarified dependencies between arith tools

separate HOL-Main image

polished code generator setup

added theory antiquotation

tuned comments;

handle _ should be avoided (spurious Interrupt will spoil the game);

added norm_export_morphism;

added exit_global, exit_result, exit_result_global; ProofContext.norm_export_morphism;

LocalTheory.exit_global;

HOL no longer depends on HOL-Plain;

setmp_noncritical;

join earlier promises first;

proper setmp_thread_data for nested execute (cf. join_loop);

promise_result: enforce strictly sequential dependencies, via serial numbers;

do not cvs update for doc test (switching to mercurial, update done outside once and for all)

use mercurial repository for isatest

thread_data: include thread name, export access; more tracing;

setmp_noncritical;

dequeue_towards: return bound for unfinished tasks;

moved release_results to future.ML; get_some: simplified via Future.release_results;

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;

Future.release_results;

more tracing;

Theory.checkpoint for main operations, admits concurrent proofs;

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;

proper transfer of theorems that involve classes being instantiated here;

HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);

eliminated polymorphic equality;

added subset operation;

Added fresh_star_const.

Added some more theorems to NominalData.

Added some more lemmas that are useful in proof of strong induction rule.

removed obsolete name convention "func"

fixed typo

clarified function transformator interface

op = vs. eq

moved future_scheduler flag to skip_proof.ML;

added future_scheduler (from thy_info.ML); prove: Goal.prove_promise if future_schedule;

simplified promise; fulfill is internal only; more robust join_futures;

simplified Thm.promise; prove_common: proper context for promise_result;

explicit checkpoint for low-level (global) theory operations admits concurrent SkipProof.prove; tuned list operations;

explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;

circumvent problem with code redundancy

clarifed redundancy policy

tuned comments;

added release_results; tuned comments;

abtract types: plain datatype with opaque signature matching; promise: join pending futures at end of theory;

prove: error with original thread position;

explicit type OrdList.T;

(temporary workaround)

(temporal deactivation)

non left-linear equations for nbe

non left-linear equations for nbe

map_force

matchess

burrow_fst

discontinued special treatment of op = vs. eq_class.eq

report: produce individual status messages;

protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy); added Kind.code map;

protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);

init: OuterKeyword.report;

prove_multi: immediate;

added promise_result, prove_promise;

Corrected call of SUBPROOF in coherent_tac that used wrong context.

fixed outer syntax

case default fallback for NBE

fixed quickcheck parameter syntax

renamed rtype to typerep

added fold_rev; tuned dest, keys;

added del_node, which is more efficient for sparse graphs;

IntGraph.del_node;

join_results: special case for empty list, works without multithreading;

added dest_deriv, removed external type deriv; misc tuning of internal deriv; more substantial promise/fulfill; promise_ord: reverse order on serial numbers; removed unused is_named; get_name: unfinished proof term;

added conditional add_oracles, keep oracles_of_proof private; added fulfill; removed unused is_named; tuned some table operations;

Thm.proof_of;

Added coherent logic prover.

New prover for coherent logic.

Added setup for coherent logic prover.

Added examples for coherent logic prover.

Examples for coherent logic prover.

made the perm_simp tactic to understand options such as (no_asm)

type thm: fully internal derivation, no longer exported; incorporate former deriv.ML as internal abstract type; added rudimentary promise interface; tuned; added is_named (does not require finished derivation);

added is_finished;

added Promise constructor, which is similar to Oracle but may be replaced later; added promise_proof; export min_proof, mk_min_proof; moved infer_derivs to thm.ML as derive_rule0/1/2; tuned oracles_of_proof; added is_named;

removed deriv.ML which is now incorporated into thm.ML;

added reject_draft;

type thm: fully internal derivation, no longer exported;

generic quickcheck framework

TEMPORARY: make batch run happy

absolute Library path

different session branches for HOL-Plain vs. Plain

temporary workaround for class constants

corrected sort intersection

some steps towards generic quickcheck framework

fixed headers

added some fragments from website

made SML/NJ happy;

Isar toplevel editor model.

future tasks: support boolean priorities (true = high, false = low/irrelevant);

output_sync is now public;

added props_text (from isar_syn.ML);

moved Isar editor commands from isar_syn.ML to isar.ML; P.props_text;

moved Isar editor commands from isar_syn.ML to isar.ML;

added Isar/isar.scala;

avoid using implicit assumptions

add theory graph to ZF document

made SMLNJ happy

jar: include sources;

tuned;

eval_term: CRITICAL due to eval_result; simplified oracle interface;

begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};

updated generated file;

simplified oracle interface;

show: non-critical testing;

added deriv.ML: Abstract derivations based on raw proof terms.

termination prover for "fun" can be configured using context data.

updated generated file;

unchecked $ISABELLE_HOME_USER/etc/settings;

use_text/use_file now depend on explicit ML name space;

threads work only for Poly/ML 5.2 or later; global ML bindings are now thread-safe;

* ML bindings produced via Isar commands are stored within the Isar context. * Command 'ML_prf' is analogous to 'ML' but works within a proof context.

added ML_prf;

updated generated file;

added inherit_env;

added map_contexts;

ML_prf: inherit env for all contexts within the proof;

shutdown only if Multithreading.available;

ML_Context.evaluate: proper context (for ML environment); use_text/use_file now depend on explicit ML name space;

ML_Context.evaluate: proper context (for ML environment);

simplified ML_Context.eval_in -- expect immutable Proof.context value;

proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);

simplified ML_Context.eval_in -- expect immutable Proof.context value; parse_code: operate on thy, which contains the ML environment;

explicit handling of ML environment within generic context; eval_wrapper: non-critical, struct_name is always Isabelle, tuned comments; eval_in/evaluate expect immutable Proof.context value; use_text/use_file now depend on explicit ML name space;

added ML_prf;

use_text/use_file now depend on explicit ML name space;

ML name space -- dummy version of Poly/ML 5.2 facility.

added ML-Systems/ml_name_space.ML;

use ML_prf within proofs;

local @{context};

moved global ML bindings to global place;

back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;