merged

added "no_atp" to Cantor's paradox

renamed "const_args" option value to "args"

temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception

updated instructions

minor doc edits

killed unimplemented type encoding "preds"

remove debugging code

removing bounded_forall code equation for characters when loading Code_Char

deriving bounded_forall instances in quickcheck_exhaustive

generalizing ensure_sort_datatype for bounded_forall instances

document "type_sys" option

if "monomorphize" is enabled, mangle the type information in the names by default

use standard tables with standard argument order;

discontinued special treatment of structure Parser -- directly accessible;

discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;

more precise propagation of reports/results through some inner syntax layers; misc reorganization;

accumulate parsetrees in canonical reverse order;

tuned;

tuned -- removed redundancy;

tuned signatures;

streamlined token list operations, assuming that the order of union does not matter;

misc tuning and clarification;

merged

document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"

refactoring generator definition in quickcheck and removing clone

use the proper contexts/simpsets/etc. in the TPTP proof method

merged

make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option

merged

Deletion of all semicolons, because they interfere with Proof General

raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.

tuned proofs

tuned proof

direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;

added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures;

show more tooltip/sub-expression markup;

show tooltip/sub-expression for entity markup;

merged

remove unnecessary prob_preserving

add prob_space_vimage

use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);

fixed accidental redefinition

save reflexivity steps in discharging Z3 Skolemization hypotheses

adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall

adding general interface for batch validators in quickcheck

remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428

scheduler for judgement day

re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end

make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option

merged

adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy

raised timeouts further, for SML/NJ

adapted parsing of session timing (cf. e86b10c68f0b)

merged

adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily

provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)

start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)

temporary workaround: filter out spurious monomorphic instances

added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default