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