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

added unfold set constant functionality to Meson/Metis -- disabled by default for now

remove unused parameter

reduced penalty associated with existential quantifiers

ensure that Auto Sledgehammer is run with full type information

fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized

don't give weights to built-in symbols

more robust exception handling in Metis (also works if there are several subgoals)

no penality for constants that appear in chained facts

gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers

improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types

tune whitespace

added configuration options for experimental features

ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)

avoid "Empty" exception by making sure that a certain optimization only is attempted when it makes sense

added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options

added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option

allow each slice to have its own type system

renamed type systems for more consistency

updated versions;

added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;

tuned;

minor adaption for scala-2.9.0.final;

proper configuration options Proof_Context.debug and Proof_Context.verbose; discontinued alias Proof.verbose = Proof_Context.verbose;

pretend that all versions of BSD are Linux, which might actually work due to binary compatibilty mode of these obsolete platforms;

more uniform naming of lemma

add a lemma about commutative append to List.thy