extending terms of Code_Evaluation by Free to allow partial terms

adhoc event handler to insert 'sendback' text into the buffer, replacing the original command

css rules for highlighting sendback text

invert event propagation flag -- in lobobrowser api, true means re-propagate

eta-expand to make SML/NJ happy

ensure that the argument of logical negation is enclosed in parentheses in THF mode

hack to obtain potable step names from Waldmeister

respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")

further reduce the number of facts passed to less used remote ATPs

added quietness flag

pass fewer relevant facts to less used remote systems

more work on parsing LEO-II proofs and extracting uses of extensionality

tuning

more work on parsing LEO-II proofs without lambdas

slightly gracefuller handling of LEO-II and Satallax output

document primitive support for LEO-II and Satallax

identify HOL functions with THF functions

started adding support for THF output (but no lambdas)

eliminated more code duplication in Nitrox

reduce code duplication in Nitrox

use \<emdash> rather than \<midarrow>

fixed de Bruijn index bug

use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things

filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations

clearer SystemOnTPTP errors

give fewer equations to Waldmeister

detect inappropriate problems and crashes better in Waldmeister

tuning -- the "appropriate" terminology is inspired from TPTP

pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding

move lemmas to Extended_Reals and Extended_Real_Limits

separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform

reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive

fun command produces warning when patterns are incomplete (somewhat analogous to primrec)

added message when Waldmeister isn't run

slightly improved documentation

improved Waldmeister support -- even run it by default on unit equational goals

fish out axioms in Waldmeister output

removed SNARK hack now that SNARK is fixed

recognize one more SystemOnTPTP error

document Waldmeister

added support for remote Waldmeister

added Waldmeister

reorganized ATP formats a little bit

tuned;

removed odd remains of low-level session management;

moved incr_boundvars; discontinued low-level term operations;

modernized and re-unified Thm.transfer;

removed obsolete material (superseded by implementation manual);

removed somewhat low-level stuff (cf. attribute "swapped" in isar-ref);

updated and re-unified classical proof methods; tuned;

tuned;

updated and re-unified classical rule declarations;

moved/updated introduction to Classical Reasoner;

tuned secref (still dangling);

updated and re-unified material on simprocs;

removed some old stuff;

tuned headings;

some material on "Generalized elimination and cases";

some material on "Structured induction proofs";

some material on "Structured Natural Deduction"; tuned;

some material on "Calculational reasoning";

tuned;

added Synopsis, with some "Notepad" material;

more accurate deps;

turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);

moved/updated basic HOL overview;

updated and re-unified (co)inductive definitions in HOL; modernized examples;

clarified current 'primrec' vs. old 'recdef'; updated examples from src/HOL/Induct;

record examples;

updated and simplified HOL datatype examples (NB: special treatment of distinctness has been discontinued in the vicinity of 542b34b178ec);

updated and re-unified HOL rep_datatype;

rearranged some sections;

updated and re-unified HOL typedef, with some live examples;

optional jedit_build/etc/user-settings enable to override defaults produced by late component initialization;

merged

add divide_.._cancel, inverse_.._iff

add surj_vimage_empty

Add restricted borel measure to {0 .. 1}

equations for subsets of atLeastAtMost

build and run Isabelle/jEdit on the spot -- requires auxiliary "jedit_build" component;

misc tuning and update;

updated versions;

added Isabelle_Process.is_active; tuned signature;

update example

name tuning

further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged

prevent unsound combinator proofs in partially typed polymorphic type systems

add lemma prob_finite_product

simp rules for empty intervals on dense linear order

merged

exercise more type systems (but only sound or quasi-sound ones)

added see also

document new type system and soundness properties of the different systems

improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything

reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts

more doc fiddling

more FAQs

make sure the Vampire incomplete proof detection code kicks in

automatically use "metisFT" when typed helpers are necessary

tuning

generate useful information for type axioms

slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous

updated FAQ

more informative message when Sledgehammer finds an unsound proof

tuned proofs

NEWS

point-free characterization of operations on finite sets

merged

names of fold_set locales resemble name of characteristic property more closely

clarified vacuous nature of predicate "transfer_morphism" -- equivalent to previous definiton

use point-free characterization for locale fun_left_comm_idem

tuned proof

Collect intro-rules for sigma-algebras * * * sets_Collect shouldn't be intro rules

the measurable sets with null measure form a ring

add some lemmas for infinite product measure

add measurable_Least

add restrict_sigma

add borel_eq_atLeastLessThan

Add formalization of probabilistic independence for families of sets

add Bernoulli space

add product of probability spaces with finite cardinality

remove double sum_over_space_real_distribution

a deeper understanding of the code generation adaptation compared to 9079f49053e5

updated option documentation

renamed "simple_types" to "simple"

since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix

tweaked ATP type systems further based on Judgment Day

honor "conj_sym_kind" also for tag symbol declarations

removed "poly_tags_light_bang" since highly unsound

distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job

reintroduce TFF workaround for limitations of actual TFF implementations (ToFoF, SNARK)

fixed empty proof detection

tuning

minor doc fixes

mention version 0.6 of Vampire, since that's what's currently available for download

better error reporting: detect missing E proofs and remove Vampire native format error

NEWS

adding Code_Char_ord to code generation regression tests

adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages

removed some obsolete text;

basic support for overpainting of text, imitating jEdit internals;

some support for token/chunk handling, imitating jEdit internals;

renamed thin to light, fat to heavy

code cleanup, better handling of corner cases

run blacklist algorithm only if slicing is on

implemented thin versions of "preds" type systems + fixed various issues with type args

use antiquotation

renamed "shallow" to "thin" and make it the default

more work on "shallow" encoding + adjustments to other encodings

generate type classes predicates in new "shallow" encoding

started implementing "shallow" type systems, based on ideas by Claessen et al.

added syntax for "shallow" encodings

provide isabellep as a method

append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism

tuned;

less fine-grained mira dependencies

mira hack for special settings on lxbroy10

no dependencies for Isabelle_makeall, which will be built in one go

clarified handling of ISABELLE_USEDIR_OPTIONS in mira

future merge of grammars, to improve parallel performance;

only show relevant timing;

timing of Theory_Data operations, with implicit thread positions when functor is applied;

tuned;

eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;

NEWS (cf. 4e8483cc2cc5);

simplified/unified method_setup/attribute_setup;

optional description for 'attribute_setup' and 'method_setup';

tuned signature;

merged

slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;

use pointfree characterisation for fold_set locale

discontinued global config options within attribute name space;

more precise warnings: observe context visibility;

modernized structure Rule_Insts;

discontinued old / unused addss' (cf. 57f364d1d3b2);

eliminated global Unsynchronized.ref; eliminated Display.string_of_thm_without_context;

proper runtime context for auto_inv_tac;

simplified BLAST_DATA;

proper Proof.context -- eliminated global operations;

just one universal Proof.context -- discontinued claset/clasimpset;

modernized functor names; tuned;

method "deepen" with optional limit;

merged

removed redundant type annotations and duplicate examples

clarified map_simpset versus Simplifier.map_simpset_global;

make ZF_cs snapshot after final setup;

proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;

do not open ML structures;

eliminated weight_ASTAR: int Unsynchronized.ref (astar_tac appears to be obsolete anyway);

misc tuning and simplification;

tuned proof;

tuned proof;

proper method_setup;

proper method_setup "split_idle";

proper method_setup "enabled";

simplified clasimpset declarations -- prefer attributes;

reduce the number of mono iterations to prevent the mono code from going berserk

tuned comment

optimized a common case

avoid "UnequalLengths" exception for special constant "fequal" -- and optimize code in the common case where no type arguments are needed

tweak E slices

make SML/NJ happy

fixed off-by-one bug

added convenience syntax

prefer Proof.context over old-style claset/simpset; canonical argument order;

prefer plain simpset operations;

removed obsolete old-style cs/css;

modernized dead code;

eliminated old-style MI_fast_css -- replaced by fast_solver with config option;

eliminated obsolete MI_css -- use current context directly;

proper method_setup;

modernized simproc_setup; misc tuning and simplification;

prefer Proof.context over old-style clasimpset;

modernized dead code;

modernized specifications;

merged

added hints and FAQs

prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior

fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP

another concession to backward compatibility

no need to use metisFT for Isar proofs -- metis falls back on it anyway

handle equality proxy in a more backward-compatible way

remove problematic Isar proof

added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around

robustly detect how many type args were passed to the ATP, even if some of them were omitted

make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types

drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation

tuning

fixed conjecture resolution bug for Vampire 1.0's TSTP output

ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded

Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it

drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines

use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.

further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up

reenabled equality proxy in Metis for higher-order reasoning

added "SMT." qualifier for constant to make it possible to reload "smt_monomorph.ML" from outside the "SMT" theory (for experiments) -- this is also consistent with the other SMT constants mentioned in this source file

reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions

unfold set constants in Sledgehammer/ATP as well if Metis does it too

do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings

renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly