tuning

slightly nicer ML interface

added convenience function

keep a record of the fixpoint equations

export ML function (needed for "primrec_new")

export ML function

corrected name

tuned proofs

type class for confined subtraction

denesting of functions

some meagure hints concerning reification

make reification part of HOL

permissive uncheck -- allow printing of malformed terms (e.g. in error messages);

Type_Annotation only works *after* uncheck (which usually requires authentic type information);

updated isatest stats;

tuned theory name

tuned rules

tuning

renamed util function

tuned;

make SML/NJ partially happy;

reflection without evaluation

decomposed reflection steps into conversions; deholified reification procedure; prefer Subgoal.FOCUS over SUBGOAL

permit multiple variable arguments in reflect

tuned

dropped vacuous prefix

combinator fold_range, corresponding to map_range

merged

more VC -> VCG

VCG is standard name

used nice syntax, removed lemma because it makes a nice exercise.

NEWS about Spec_Check

tuned headers;

tuned messages -- some attempts to observe Isabelle output channel semantics;

less verbosity -- do not print final ();

tuned -- dynamic ML context is updated incrementally (see also e7c47fe56fbd);

tuned;

toplevel invocation via implicit ML compilation context;

more direct Context.setmp_thread_data for one-way passing of context;

tuned;

tuned;

do not open ML structures;

prefer separate 'ML_command' for parallel evaluation;

simplified context and data management -- plain ctxt: Proof.context is default for most operations;

more conventional spelling and grammar;

minor tuning -- more linebreaks;

removed pointless comment -- NB: Isabelle output is message-oriented with implicit line-boundaries;

standardized aliases;