tuning

tuning

tuned

tuned variable names

tuned

tuning

tuning

[mq]: tuning

tuning

tuning

tuning

tuning

fixed failure in coinduction rule tactic

too much qualification is like too little

tuning

tuning

tuning

merge

tuning

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;

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;

do not handle arbitrary exceptions;

added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;

merged

tuned signature;

tuned signature; tuned;

misc tuning;

prefer existing beta_eta_conversion;

more standard fold/fold_rev;

tuned import;

misc tuning;