dropped redundant lemma

syntactically tuned

prefer plain bool over dedicated type for binary digits

tuned

compile + reduce problem size by a notch

generate exhaust from nchotomy

made tactic work with theorems with multiple assumptions

renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)

express weak pullback property of bnfs only in terms of the relator

merged

tuned

reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)

tuning whitespace

recognize datatype reasoning in SPASS-Pirate

note manually proved exclusiveness property

note exhaust proof obligation

compile

implemented 'exhaustive' option in tactic

tuning

tuning

tuning 'case' expressions

don't do 'isar_try0' if preplaying is off

more data structure refactoring

data structure rationalization

tuning

refactored preplaying outcome data structure

distinguish not preplayed & timed out

pick up tfree/tvar type from SPASS-Pirate proof

tuning

extended ATP types with sorts

removed debugging output

honor SPASS-Pirate type arguments

made SML/NJ-friendlier (hopefully)

made timeouts in Sledgehammer not be 'option's -- simplified lots of code

simplified data structure

prevent curl's output to interfere with the prover's output

tuning

merge

parse SPASS-Pirate types

merged

added lemma

merge

pass down user input in more cases in order to preserve "let"s etc.

pass auto-proved exhaustiveness properties to tactic; rightly use "%_. False" instead of undefined for unspecified conditions; get rid of ugly "if True then ... else Code.abort" in auto-generated code equations;

merge

changed pirate port

fixed variable confusion introduced by 'tuning' change 565f9af86d67

made SML/NJ happier

try 'auto' first -- more likely to succeed

new port

tuning

generate type classes for tfrees

modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property

avoid clashes of fact names

initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts

reduced cardinals dependencies of (co)datatypes

tighter bnf bounds for (co)datatypes

tuned

tuning

removed workaround

tuning

primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)

NEWS

merged

lemmas about divideR and scaleR

monotonicity of rounding and truncating float

Float: prevent unnecessary large numbers when adding 0

additional definitions and lemmas for Float

additional lemmas

summarized notions related to ordered_euclidean_space and intervals in separate theory

pragmatic executability of instance prod::{open,dist,norm}

introduced ordered real vector spaces

remove redundant constants

ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order

prefer box over greaterThanLessThan on euclidean_space

made SML/NJ happier

fixed source of 'Subscript' exception

handle Skolems gracefully for SPASS as well

move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)

reverse Skolem function arguments

correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference

fixed confusion between 'prop' and 'bool' introduced in 4960647932ec

generalize method list further to list of list (clustering preferred methods together)

store alternative proof methods in Isar data structure

tuning

added 'meson' to the mix

tuning

made SML/NJ happy

use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning

generate proper succedent for cases with trivial branches

tuning

simplify generated propositions

use 'prop' rather than 'bool' systematically in Isar reconstruction code

tuning

use 'arith' when appropriate in Z3 proofs

robustness in degenerate case + tuning

use simplifier for rewrite

more aggressive merging

implemented Z3 skolemization

inline Z3 hypotheses

merge

merge

merged

better handling of Z3 proof blocks

disambiguation of interpretation prefixes

more algebraic terminology for theories about big operators

more antiquotations;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;

merged

maintain morphism names for diagnostic purposes;

tuned -- prefer canonical argument order of fold_rev;

proper simplifier context; more standard "cert";

tuned;

tuned whitespace;

made SML/NJ happy + whitespace tuning

clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;

merged

discontinued legacy_isub_isup;

clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;

skeleton for Simplifier trace by Lars Hupel;