revisiting mk_equation functions and refactoring them in exhaustive quickcheck

creating a general mk_equation_terms for the different compilations

adding an even faster compilation scheme

theory definitions for fast exhaustive quickcheck compilation

new compilation for exhaustive quickcheck

tuned;

present type variables; tuned;

unparse: more accurate markup for syntax consts, notably binders;

notation: proper markup for type constructor / constant;

tuned signature;

more accurate markup for syntax consts, notably binders which point back to the original logical entity; tuned;

discontinued Syntax.max_pri, which is not really a symbolic parameter;

CONST syntax with positions;

moved CONST syntax/translations to their proper place;

simplified Pure syntax bootstrap;

renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned;

merged

raised timeout further, for SML/NJ

discontinued special treatment of structure Lexicon;

discontinued special status of structure Printer;

discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;

discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;

more antiquotations;

removed outdated text (cf. 84a3f86441eb);

explicit structure Syntax_Trans; discontinued old-style constrainAbsC;

tuned presentation;

report literal tokens according to parsetree head; some attempts to stack parsetrees in proper order;

simplified read_term vs. read_prop;

tuned signature;

constant =?= no longer exists (cf. 8c09e1fa24a7);

clarified sources -- removed odd comments;

tuned signature;

merged

removing decrement of cardinality in quickcheck -- counting cardinalities starts at 1

removing instantiation exhaustive for unit in Quickcheck_Exhaustive

correcting bounded_forall construction; tuned

dropped unused lemmas; proper Isar proof

further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind

make new Skolemizer more robust

tuned comment

discontinued user-defined token translations; tuned signature;

simplified printer context: uniform externing and static token translations;

clarified Pretty.mark; added Pretty.mark_str, Pretty.marks_str convenience;

parallel parsing of big specifications;

separate structure Term_Position; dismantled remains of structure Type_Ext;

type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);

moved type syntax translations to syn_trans.ML;

made SML/NJ happy (cf. 578a51fae383);

merged

merged

changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)

prove measurable_into_infprod_algebra and measure_infprod

Rename extensional to extensionalD (extensional is also defined in FuncSet)

eliminated slightly odd Syntax.rep_syntax;

more abstract print translation;

more abstract syntax translation;

tuned;

explicit Syntax.tokenize, Syntax.parse;

eliminated odd object-oriented type_context/term_context; export ProofContext.intern_skolem;

simplified standard parse/unparse;

discontinued old-style Syntax.constrainC;

typed_print_translation: discontinued show_sorts argument;

misc tuning and simplification;

moved unparse material to syntax_phases.ML;

more symbol abbrevs;

renamed Standard_Syntax to Syntax_Phases;

moved decode/parse operations to standard_syntax.ML; tuned;

separate module for standard implementation of inner syntax operations;

moved Isar/local_syntax.ML to Syntax/local_syntax.ML;

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