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;

updated generated file;

wf_finite_psubset[simp], in_finite_psubset[simp]

Public interface to interpretation morphism.

moved term_of syntax to separate theory

removed obsolete theory

added quickcheck.ML

tuned comments;

multithreading for Poly/ML 5.1 is no longer supported;

tuned;

updated system manual;

Proof General / Emacs interface wrapper;

Proof General: option -I is obsolete;

added PROOFGENERAL_HOME;

separate emacs tool for Proof General / Emacs;

added quickcheck stub

removed babel again

celver code lemma avoid type ambiguity problem with Haskell

a sophisticated char/nibble conversion combinator

moved term_of syntax to separate theory

SimpleThread.fork;

Simplified thread fork interface.

added Concurrent/simple_thread.ML;

updated generated file;

misc tuning and modernization;

check setting and tool; added file;

Clearer separation of interpretation frontend and backend.

No interpretation of locale with dangling type frees.

Do not rely on locale assumption in interpretation.

The metis method now fails in the usual manner, rather than raising an exception, if it determines that it cannot prove the theorem.

Fixed typo in locale declaration.

added babel

explicit size of characters

dropped superfluous code lemmas

evaluation using code generator

generic value command

converted symbols.tex;

tuned;

converted misc.tex;

tuned;

generated files;

converted present.tex;

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

load underscore package after iman etc.;

tuned comment;

added formal markup for setting, executable, tool;

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

converted basics.tex to theory file;

added isatt markup;

New outline for codegen tutorial -- draft

added extern_fact (local or global); more procise printing of fact names;

print raw (internal) result names;

more procise printing of fact names;

pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;

cancel, shutdown: notify_all;

finish: Future.shutdown last;

eliminated requests, use global state variables uniformly; more robust shutdown;

finish: Future.shutdown;

added is_empty;

shutdown: global join-and-shutdown operation; reduced trace_active; scheduler_fork: always notify; tracing for thread exit; unique ids for workers;