merged

tuned

increased stack limits (again, cf. d9cf3520083c and 77c3e74bd954);

explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;

tuned proofs;

retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;

prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future;

recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;

proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);

improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory

in a local context, also the free variable case needs to be analysed default tip

speed-up proof;

more abstract datatype stamp, which avoids pointless allocation of mutable cells;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

simplified -- empty_ss already contains minimal mksimps;

Abstract interpretation is now based uniformly on annotated programs, including a collecting and a small step semantics

tuned;

tuned;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

tuned;

updated according to bdcaa3f3a2f4;

updated proof;

tuned

remove outdated comment

NEWS;

simplified read_instantiate -- no longer need to assign values, since rule attributes are now static;

drop vacuous decls;

tuned;

tuned header;

misspelled name

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