no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle

Mirabelle: handle possible parser exceptions, emit suitable log message

merged

sledgehammer's temporary files are removed properly (even in case of an exception occurs)

merged

tuned the simp rules for Int involving insert and intervals.

Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)

Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names

merged

apply metis with found theorems in case sledgehammer was successful

propagate theorem names, in addition to generated return message

misc tuning;

eliminated hard tabs;

moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala; renamed object IsabelleSyntax to Isabelle_Syntax;

merged

fixed HOLogic.stringT

merged

tuned proofs

tuned proofs

tuned proofs

tuned proofs

tuned proofs

tuned proofs

tuned proofs

tuned proofs

Turned "x <= y ==> sup x y = y" (and relatives) into simp rules

New option ForceSystem that makes sure we *really* get the system we ask for

selectable prover for sledgehammer, proper environment lookup

discontinued Display.pretty_ctyp/cterm etc.;

modernized messages -- eliminated ctyp/cterm operations;

removed spurious invocations of atp_minimize;

removed obsolete print_ctyp, print_cterm;

modernized messages -- eliminated old Display.print_cterm;

SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably; misc tuning and cleanup;

misc updates and tuning;

PDF_VIEWER: more Unix-ish behaviour on Mac OS;

merged

New example: IMP

merged

code generator: quantifiers over {_.._::int} and {_..<_::nat} are now translated into (tail recursive) loops - no list is built.

more stats;

tuned tracing;

merged

avoid macbroy21 for now -- hardware problems;

tuned code generation for lists

merged

got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.

merged

merged

removed unused theorem finite_Atleast_Atmost

merged

Derivative of general reverses

merged

new interval lemma CCS example for predicate compiler

merged

Simplified some proofs using metis.

merged

sledgehammer used to streamline protocol proofs

Put back characters that had been erased by Emacs

added further conversions and conversionals

merged

new lemmas

some examples for giving measures manually

stricter condition for (binary) integer relation

more quoting for shell variables, canonical isabelle process

keep the modified (tested) theory, added an explicit reference to the modified theory in the generated log file

do not introduce additional newlines

tuned;

generalized settings;

removed jedit setup -- now a self-contained component (external);

less ambitious array operations -- for improved compatibility with older versions of bash;

function splitarray: splightly more abstract version that accomodates older bashes;

fix IsaMakefile, removing mirabelle (not in HOL/ex/ROOT.ML anyway)

added Mirabelle to NEWS

merged

disabled refute action (needs changes in the code of refute)

split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)

moved Mirabelle to HOL/Tools

moved Mirabelle to HOL/Tools

Mirabelle tool script conforming to standard Isabelle tool interface, tidied Perl script, moved ML sources to Tools subdirectory

made Mirabelle a component

A few Isar scripts

additional checkpoints avoid problems in error situations

tuned

removed atp_minimize invocation

reverted accidential corruption of superscripts introduced in a508148f7c25

merged

inserted space into message

formally stylized

formally stylized

corrected Pair to Char

merged

Fixed a bug where the simplifier would hang on lemma "f a = M { nat j |j. 0 <= j & j < f b}" pre_decomp/pre_tac no longer split terms that contain (non-locally) bound variables (e.g., "nat j" in the above example).

merged

Removal of redundant settings of unification trace and search bounds.

Demonstrations of sledgehammer in protocol proofs.

added PARALLEL_CHOICE, PARALLEL_GOALS;

merged

SOS: function to set default prover; output channel changed

interrupt handler for neos csdp client

clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;

updated generated document

dropped temporary adjustments to non-working eta expansion in recfun_codegen.ML

proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML

merged

temporary adjustment to dubious state of eta expansion in recfun_codegen

properly merged

same_typscheme replaces ugly common_typ_eqns

moved all technical processing of code equations to code_thingol.ML

added map_transpose

merged

attempt to move desymbolization to translation

added a somehow clueless comment

repair mess produced by resolution afterwards

using certify_instantiate

merged

cleaned up variable desymbolification and argument expansion

more appropriate printing of function terms

improved handling of parameters

path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples