avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs

interpret "max_facts" argument in a slice-dependent fashion, instead of forcing the same number of facts to all slices

delete also predicates on relations when hiding an implementation of an abstract type

reintroduced crucial sorting accidentally lost in 962190eab40d

compile

provide two modes for MaSh driver: linearized or real visibility

implement (more) accurate computation of parents

tuning

split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations

simplified byline, isar_qualifier

tuned code: factored out parent computation

tuned code

simplify definition as sort constraints ensure finiteness (thanks to Jesus Aransay)

fundamentals about discrete logarithm and square root

Sieve of Eratosthenes

note on parallel computation

corrected and clarified Code_Binary_Nat vs. Code_Target_Nat

simplified construction of upto_aux

merged

restored proper order of NEWS entries (lost due too long-waiting patches)

CONTRIBUTORS

tail recursive code for function "upto"

tuning

repaired collateral damage from 4f0147ed8bcb

Backed out changeset: 3fe7242f8346, many proofs (e.g. in Extended_Real and Approximation) rely on coercions not being lifted over sets

dropped now obsolete hint; a few words on theory IArray; dropped reference to obsolete theory Efficient_Nat

attempt to re-establish conventions which theories are loaded into the grand unified library theory; four different code generation tests for different code setup constellations; augment code generation setup where necessary

systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char

coercions between base types can be lifted to sets

annotate obtains with types

merge

made check for conjecture skolemization sound

use safe var index

merged

more type class instances for Numeral_Type (contributed by Jesus Aransay)

added lemma

merge

merge

skolemize conjecture properly in Isar proof

tuning -- refactoring in preparation for handling skolemization of conjecture

removed dead weight from data structure

tuned code

tuned code

less customary term_of conversions; spurious side effect on method reflection

two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one

explicit code equation for integer_of_nat

extended stream library

merged

partially revert 0dac0158b8d4 as it too aggressively spreads card_UNIV type class whose dictionary constructions can slow down generated code; provide better error messages instead for card and subseteq

killed legacy alias

updated news

avoid crude/wrong theorem comparision

tuned code

more MaSh tracing

tuning

fixed metis_steps_total - was off by one

preplay subblocks

renamed sledgehammer_shrink to sledgehammer_compress

dont skolemize conjecture

introduced subblock in isar_step datatype for conjecture herbrandization