tuned defs

avoid duplicate call to "mk_fold_rec_args_types" function

continuation of f461dca57c66

renamed ML variables

tuned record field names to avoid confusion between low-level and high-level constants/theorems

tuned signature

support induction principles with multiple occurrences of the same type in "fpTs" and (hopefully) with loss of recursion (e.g. primrec definition of is_nil, where the IH can be dropped)

tuned ML variable names

transfer rule for listsum

more reflexivity rules (for OO)

tuning

avoid code duplication

eliminated dead argument

one less flaky "fpTs" check (flaky in the presence of duplicates in "fpTs", which we want to have in "primrec")

tuning

simpler, more robust iterator goal construction code

tuning

reverted 23929f647f79 -- not needed after all

killed dead code

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;