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;

prefer existing beta_eta_conversion;

more standard names;

simplified method setup;

tuned -- prefer terminology of tactic / goal state;

tuned;

misc tuning;

tuned;

tuned signature;

stay within regular tactic language -- avoid operating on whole proof state;

standardized aliases;

space between minus sign and number for large negative number literals causes NumberFormatException at run-time

tuned

relational version of HoareT

obsolete;

resolve_inc_tyvars: back to old behavior before 0fa3b456a267 where types of equal Vars are *not* unified -- recover last example in src/HOL/Metis_Examples/Clausification.thy;

more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);

tuned signature -- more explicit flags for low-level Thm.bicompose;

unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification;

tuned signature;

backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;

observe type annotations in print translations as well, notably type_constraint_tr';

make SML/NJ happy;

tuning

more work on general recursors

tuning (use lists rather than pairs of lists throughout)

generalized recursors, effectively reverting inductive half of c7a034d01936

tuning

merged

explicit support for type annotations within printed syntax trees; eliminated obsolete show_free_types;

more explicit Printer.type_emphasis, depending on show_type_emphasis; tuned signature;

tuning (refactoring)

refactored triplicated functionality

tuning -- avoided unreadable true/false all over the place for LFP/GFP

merge

don't create needless constant

merged

fixed broken Cardinals and BNF due to Order_Union

no confusing special behavior in debug mode

tuned Nitpick message to be in sync with similar warning from Kodkod

merged

merged Well_Order_Extension into Zorn

removed junk (cf. 667961fa6a60);

exported ML function

redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])

clean up list of theorems

removed needless comment (yes, sum_case_if is needed)

tuned

actually test theory Order_Union;

more direct notation;

merged

more literal tokens, e.g. "EX!";

report markup for ast translations;

tuned;

tuned;

discontinued obsolete show_all_types;

added Ordered_Union

fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)

well-order extension (by Christian Sternagel)

modernized Zorn (by Christian Sternagel)

merged

more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);

instantiate types as well (see also Thm.first_order_match);