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