eliminated obsolete "standard";

eliminated obsolete "standard";

eliminated obsolete "standard";

eliminated obsolete "standard";

eliminated obsolete "standard";

explicit is better than implicit;

eliminated obsolete "standard";

tuned signature;

'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;

updated comment;

more uniform signature;

uniform cert_vars/read_vars;

eliminated dead code;

clarified certify vs. sharing;

tuned;

NEWS;

added ML antiquotation @{attributes};

merged

made SML/NJ happy

simplified Locale.add_thmss, after partial evaluation of attributes;

misc tuning;

tuned;

refined partial evaluation of attributes: avoid duplication of facts for plain declarations; tuned;

discontinued slightly odd write_prv, which would still write .prv files the first time, and deprive add-on tools from date stamp change (cf. 157e74588c49);

do not store vacuous theorem specifications -- relevant for frugal local theory content; tuned;

put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory; tuned;

sequential lemmas to accomodate static rule attributes;

partial evaluation of locale facts leads to static scoping of rule attributes;

tuned message;

gave SML/NJ a chance

more robust options

adding another example for lifting definitions

improving header

more "metis" calls in example

be more silent when auto minimizing

less offensive terminology

more "metis" calls in example

minor textual improvement

pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones

wrap lambdas earlier, to get more control over beta/eta

move eta-contraction to before translation to Metis, to ensure everything stays in sync

avoid that var names get changed by resolution in Metis lambda-lifting

better threading of type encodings between Sledgehammer and "metis"

fixed bugs in lambda-lifting code -- ensure distinct names for variables

protect prefix against variant mutations

example cleanup

example cleanup

don't propagate user-set "type_enc" or "lam_trans" to Metis calls

don't needlessly pass "lam_lifted" option to "metis" call for SMT proof

avoid spurious messages in "lam_lifting" mode

eta-contract to avoid needless "lambda" wrappers

quiet down SMT

more aggressive lambda hiding (if we anyway need to pass an option to Metis)

updated Sledgehammer docs

don't pass "lam_lifted" option to "metis" unless there's a good reason

no needless reconstructors

removed more clutter

removed needless baggage

Word.thy: reduce usage of numeral-representation-dependent thms like number_of_is_id in proofs

merged

Groups.thy: generalize several lemmas from class ab_group_add to class group_add

HOL-Word: removed more duplicate theorems

HOL-Word: removed many duplicate theorems (see NEWS)

Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations

move definitions of bitwise operators into appropriate document section

HOL-Word: add simp rules for bin_rest, bin_last; shorten several proofs

HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'

simplify implementation of approx_reorient_simproc

name simp theorems st_0 and st_1

remove redundant simp rules plus_enat_0

eliminated slightly odd Rep' with dynamically-scoped [simplified]; tuned proofs;

partial evaluation in invisible context;

adding a preliminary example to show how the quotient_definition package can be generalized

tuned header

adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition

simplify some proofs

Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead

merged

rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests

remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead

simplify proof of word_of_int; remove several now-unused lemmas about Rep_Integ

retain mixed attributes as dynamic theorem expression, but disallow subsequent static rules;

clarified Attrib.partial_evaluation;

tagging is not stable under morphisms and need to be replayed dynamically (mixed_attribute);

compile

compile

compile

give each time slice its own lambda translation

thread in additional options to minimizer

make metis reconstruction handling more flexible

document metis options better

fixed typo

document "lam_trans" option

nicer bullets

parse lambda translation option in Metis

rename the lambda translation schemes, so that they are understandable out of context

rename configuration option to more reasonable length

continued implementation of lambda-lifting in Metis

disable debugging output

use consts, not frees, for lambda-lifting

started implementing lambda-lifting in Metis

improved generators for rational numbers to generate negative numbers; added examples

tuned

remove one more old-style semicolon

Metis_Examples/Big_O.thy: add number_ring class constraints, adapt proofs to use cancellation simprocs

remove old-style semicolons

avoid theorem references like 'semiring_norm(111)'

merged

merged

Parametric_Ferrante_Rackoff.thy: restrict to class number_ring, replace '1+1' with '2' everywhere

avoid numeral-representation-specific rules in metis proof

merged

remove sorry, otherwise it breaks the testboard

cleaned up float theories; removed duplicate definitions and theorems

enforce quick_and_dirty in Code_Real_Approx_By_Float

some support for partial evaluation of attributed facts;

tuned;

eliminated dead code;

inner syntax positions for string literals;

less confusion subexpression markup;

pass positions for named targets, for formal links in the document model;

simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;

more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);

merged

setting up exhaustive generators which are used for the smart generators

add Code_Real_Approx_By_Float

merged

remove lemma float_remove_real_numeral, which duplicated Float.float_number_of

remove unnecessary number-representation-specific rules from metis calls; speed up another proof

avoid confusing selector output

remove unsound line in Nitpick's "rat" setup

tuned proofs;

merged

removed some old-style semicolons

index markup elements for more efficient cumulate/select operations;

tuned;

tuned markup -- prefer user-perspective;

tuned specifications and proofs;

more precise type;

refined Markup_Tree implementation: stacked markup within each entry; tuned;

tuned signature; express select in terms of cumulate;

tuned signature;

merged

merged

abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite; add tests for abel_cancel simprocs

use simproc_setup for the remaining nat_numeral simprocs

use simproc_setup for more nat_numeral simprocs; add simproc tests

using more conventional names for monad plus operations

more tooltip content;

added markup_cumulate operator;

depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);

tuned;

more abstract Markup_Tree;

prefer statically typed Text.Markup;

discontinued entity text color, notably historic red for classes; tuned entity names;

more scalable Proof_Context.prepare_sorts; reverted a97251eea458 -- uniform position constraints independently of accidental source positions (e.g. TTY vs. document);

increasing values_timeout to avoid failures of isatest with HOL-IMP

renaming example invocations: tester predicate_compile is renamed to smart_exhaustive

adding CPS compilation to predicate compiler; removing function_flattening reference; new testers smart_exhaustive and smart_slow_exhaustive; renaming PredicateCompFuns to Predicate_Comp_Funs;

adding option allow_function_inversion to quickcheck options

more efficient prepare_sorts -- bypass encoded positions;

suppress irrelevant positions;

more generous margin;

pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;

tuned signature;

discontinued unused Thm.compress (again);

renewed prolog-quickcheck

adding some test cases for preprocessing and narrowing

adding a minimalistic preprocessing rewriting common boolean operators; tuned

merged

merged

tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1

use simproc_setup for some nat_numeral simprocs; add simproc tests

add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type s not in this class); test simprocs using most general type classes instead of just int and rat.

simultaneous check; tight maxidx;

avoid separate typ_check phases, integrate into main term_check 0 instead (cf. its Syntax.check_typs in Type_Infer_Context.prepare);

clarified singleton_fixate: intersection with supersort is identity, only replace actual type inference parameters; tuned reject_other, after_infer_fixate;

misc tuning and simplification;

misc tuning;

tuned signature; tuned;

quickcheck invocations in mutabelle must not catch codegenerator errors internally

sort assignment before simultaneous term_check, not isolated parse_term; prefer Syntax.read_typ over Syntax.parse_typ, to include check phase for sort assignment; simplified Syntax_Phases.decode_sort/decode_typ; discontinued unused Proof_Context.check_tvar;

tuned;

avoid inconsistent sort constraints;

localized Record.decode_type: use standard Proof_Context.get_sort; clarified Record.varifyT: more convential use of maxidx + 1;

tuned signature -- emphasize internal role of these operations;

proper configuration option; tuned;

tuned layout;

more precise messages with the tester's name in quickcheck; tuned

quickcheck fails with code generator errors only if one tester is invoked

removing extra arguments

removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result