the configuration option 'trace_simp' now uses the reference of the ProofGeneral settings menu as (dynamic) default value

merged

implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;

make SML/NJ happy

pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;

static defaults for configuration options;

configuration options admit dynamic default values;

tuned;

do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase;

use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;

merged

re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)

Typedef.info: separate global and local part, only the latter is transformed by morphisms;

merged

added reference to Trace Simp Depth.

merged

Automated lifting can be restricted to specific quotient types

moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;

disallow premises in primitive Theory.add_def -- handle in Thm.add_def; eliminated obsolete Sign.cert_def; misc tuning and clarification;

disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;

added Term.fold_atyps_sorts convenience;

moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;

eliminated old-style Theory.add_defs_i;

slightly more general simproc (avoids errors of linarith)

merged

updated SMT certificates

made renamings stable under name changes in the original problem (uninterpreted names are irrelevant to the SMT solver, and caching of SMT certificates relies on irrelevancy of renamings)

replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context

merged

Added finite measure space.

tuned white space;

more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;

low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);

merged

merged

make Mirabelle happy again

revert debugging output that shouldn't have been submitted in the first place

added support for Sledgehammer parameters; this change goes hand in hand with f8c738abaed8

simplify Nitpick parameter parsing code a little bit + make compile

add new file "sledgehammer_util.ML" to setup

honor the newly introduced Sledgehammer parameters and fixed the parsing; e.g. the prover "e_isar" (formely "e_full") is gone, instead do sledgehammer [atps = e, isar_proof] to get the same effect

added a syntax for specifying facts to Sledgehammer; e.g., sledgehammer (add: foo del: bar) which tells the relevance filter to include "foo" but omit "bar".

leverage code now in Sledgehammer

added options to Sledgehammer; syntax: sledgehammer [options] goal_no, where "[options]" and "goal_no" are optional

make "sledgehammer" and "atp_minimize" improper commands

Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS); officially export weaken as Sorts.classrel_derivation; tuned comments;

removed unused AxClass.of_sort derivation;

more precise dependencies;

merged

merged

removed predicate_compile_core.ML from HOL-ex session

added predicate compiler quickcheck examples to new session Predicate_Compile_Examples

adopting examples to Library move

moved further predicate compile files to HOL-Library

added simple setup for arithmetic on natural numbers

removing uncommented examples in setup theory of predicate compile quickcheck

moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session

slightly more logical bootstrap order -- also helps to sort out proof terms extension;

remove ancient continuity tactic

removed Cache_IO component

updated SMT certificates

inhibit invokation of external SMT solver

more precise dependencies

cache_io is now just a single ML file instead of a component

use internal SHA1 digest implementation for generating hash keys

remove component Cache_IO (external dependency on MD5 will be replaced by internal SHA1 digest implementation)

merged

minimize dependencies

sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod

use ml_platform instead of ml_system to distinguish library names

merged

use LONG rather than INT to represent the C datatype size_t

merged

remove continuous let-binding function CLet; add cont2cont rule ordinary Let

move letrec stuff to new file HOLCF/ex/Letrec.thy

more accurate dependencies;

even less ambitious isatest for smlnj;

Unhide measure_space.positive defined in Caratheodory.

Generate image for HOL-Probability

updated Thm.add_axiom/add_def;

completely remove constants cpair, cfst, csnd

use Pair instead of cpair in Fixrec_ex.thy

use Pair instead of cpair

define CLetrec using Pair, fst, snd instead of cpair, cfst, csnd

define csplit using fst, snd

convert lemma fix_cprod to use Pair, fst, snd

remove unused syntax for as_pat, lazy_pat

add lemmas fst_monofun, snd_monofun

use Pair instead of cpair

use fixrec_simp instead of fixpat

use Pair, fst, snd instead of cpair, cfst, csnd

remove admw predicate

remove contlub predicate

merged

error -> raise Fail

merged

merged

merged

remove unused adm_tac.ML

avoid dependence on adm_tac solver

remove obsolete holcf_logic.ML

fix ML warning in domain_library.ML

fix ML warnings in repdef.ML

fix ML warnings in fixrec.ML

fix ML warnings in pcpodef.ML

fix LaTeX overfull hbox warnings in HOLCF document

remove LaTeX hyperref warnings by avoiding antiquotations within section headings

explicit Simplifier.global_context;

recovered header;

eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;

inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;

use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);

added Specification.axiom convenience;

detect OFCLASS() axioms in Nitpick; this is necessary now that "Thy.all_axioms_of" returns such axiom (starting with change 46cfc4b8112e)

merged

contextifying the compilation of the predicate compiler

removed unused Predicate_Compile_Set

avoiding fishing for split_asm rule in the predicate compiler

contextifying the proof procedure in the predicate compiler

making flat triples to nested tuple to remove general triple functions

reduced the debug output functions from 2 to 1

some improvements thanks to Makarius source code review

adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises

enabling a previously broken example of the predicate compiler again

improving handling of case expressions in predicate rewriting

adding depth_limited_random compilation to predicate compiler

a new simpler random compilation for the predicate compiler

reviving the classical depth-limited computation in the predicate compiler

cleaning the function flattening

generalized split transformation in the function flattening

only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code

restructuring function flattening

renaming mk_prems to flatten in the function flattening

simplifying function flattening

removed warning_count (known causes for warnings have been resolved)

remove the iteration counter from Sledgehammer's minimizer

merged

start work on direct proof reconstruction for Sledgehammer

renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar"; "full" sounds like "full types" or something, not like a structured Isar proof -- at some point I hope to make this an option that's orthogonal to the prover

move all ATP setup code into ATP_Wrapper

move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later

more Sledgehammer refactoring

use a proof context instead of a local theory

provide a hook to safely manipulate verification conditions

replaced old-style Drule.add_axiom by Specification.axiomatization

removed e-mail address from error message

merged

tuned whitespace

handle hidden polymorphism in class target (without class target syntax, though)

replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;

replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;

add_axiom: axiomatize "unconstrained" version, with explicit of_class premises; more uniform add_axiom/add_def;

Logic.mk_of_sort convenience;

more explicit invented name;

minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';

do not open ML structures;

modernized overloaded definitions;

standard headers;

slightly more uniform definitions -- eliminated old-style meta-equality;

eliminated old constdefs;

corrected setup for of_list

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

added lemma infinite_Un

Check that argument is not a 'Bound' before calling fastype_of.

typedef etc.: no constraints;

allow sort constraints in HOL/typedef;

allow sort constraints in HOL/typedef and related HOLCF variants;

OuterParse.type_args_constrained;

support type arguments with sort constraints;

typedecl: no sort constraints; prefer Name.invents over old-style Name.variant_list;

eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;

typedecl: no sort constraints;

eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types); allow sort constraints; misc tuning and clarification;

Added product measure space

added type constraints to make SML/NJ happy

merged

fix Mirabelle after renaming Sledgehammer structures

merged

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

renamed "ATP_Linkup" theory to "Sledgehammer"

renamed Sledgehammer structures

move Sledgehammer files in a directory of their own

merged

dropped odd interpretation of comm_monoid_mult into comm_monoid_add

lemma swap_inj_on, swap_product

meaningful transfer certificate

dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule

updated certificate

dropped odd interpretation of comm_monoid_mult into comm_monoid_add

added locales folding_one_(idem); various streamlining and tuning

generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add

tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)

added one-entry cache around Kodkod invocation

merged

solve error in "Nitpick_Mono" + short path when no finite functions are inferred

minor additions to Nitpick docs

NEWS: Nat_Bijection library

document "nitpick_choice_spec" attribute

fix typo in "nitpick_choice_spec" attribute name (singular, not plural)

added support for "specification" and "ax_specification" constructs to Nitpick

rollback of local typedef until problem with type-variables can be sorted out; fixed header

adjusted to changes in Finite_Set

merged

merged

tuned inductions

tuned;

moved old Sign.intern_term to the place where it is still used;

preserve full const name more carefully, and avoid slightly odd Sign.intern_term;

replaced type_syntax/term_syntax by uniform syntax_declaration;

merged

corrected disastrous syntax declarations

added stmaryrd for isasymSqinter

use headers consistently

no_document for theory Countable

old domain package also defines map functions

separate map-related code into new function define_map_functions

removed Local_Theory.theory_result by using local Typedef.add_typedef

tuned comment;

observe standard header format;

expose formal text;

localized @{class} and @{type};

move functions into holcf_library.ML

simplify definition of when combinators

declare case_names for various induction rules

add case name 'adm' for infinite induction rules

renamed some lemmas generated by the domain package

use Simplifier.context to avoid 'no proof context in simpset' errors from fixrec_simp after theory merge

fixpat command prints legacy_feature warning

merged

pass binding as argument to add_domain_constructors; proper binding for case combinator

pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names

pass take_info as argument to Domain_Theorems.theorems

replace some string arguments with bindings

more consistent use of qualified bindings

avoid unnecessary primed variable names

remove redundant lemmas

fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy

fixrec now generates qualified theorem names

no_document for Infinite_Set in HOLCF

removed unused Args.maxidx_values and Element.generalize_facts;