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;

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;