shorten the code by conditional function application

fail for problems containg the universal sort (as those problems cannot be atomized)

renamed "smt_record" to "smt_fixed" (somewhat more expressive) and inverted its semantics

Added Information theory and Example: dining cryptographers

simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle

removed (latex output) notation which is sometimes very ugly

merged

added missing mult_1_left to linarith simp rules

tuned proof (no induction needed); removed unused lemma and fuzzy comment

isatest: basic setup for cygwin-poly on atbroy102;

slightly more standard dependencies;

merged

tuned many proofs a bit

merged

documented [[trace_simp=true]]

add missing goal argument

adapt syntax of Sledgehammer options in examples

merged

fixed layout of Sledgehammer output

added "modulus" and "sorts" options to control Sledgehammer's Isar proof output

make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"

get rid of Polyhash, since it's no longer used

remove use of Polyhash; the new code is slightly faster. Also, "subtract_cls" now has canonical argument ordering.

reintroduce efficient set structure to collect "no_atp" theorems

made "theory_const" a Sledgehammer option; by default, it's true for SPASS and false for the others. This eliminates the need for the "spass_no_tc" ATP, which can be obtained by passing "no_theory_const" instead.

added "respect_no_atp" and "convergence" options to Sledgehammer; these were previously hard-coded in "sledgehammer_fact_filter.ML"

adding MREC induction rule in Imperative HOL

made smlnj happy

adding examples of function predicate replacement and arithmetic examples for the predicate compiler; tuned

adopting specialisation examples to moving the alternative defs in the library

adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler

no specialisation for predicates without introduction rules in the predicate compiler

improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler

activating the signature of Predicate_Compile again which was deactivated in changeset d93a3cb55068 for debugging purposes

adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler

clarifying the Predicate_Compile_Core signature

adding signature to Predicate_Compile_Aux; tuning Predicate_Compile_Aux structure

putting compilation setup of predicate compiler in a separate file

simplify fold_graph proofs

NEWS

removed dead code; fixed typo

switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)

merged

adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet

tuned

generalized alternative functions to alternative compilation to handle arithmetic functions better

correcting alternative functions with tuples

no specialisation for patterns with only tuples in the predicate compiler

adding registration of functions in the function flattening

added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler

adding specialisation examples of the predicate compiler

adding specialisation of predicates to the predicate compiler

returning an more understandable user error message in the values command

adding Lazy_Sequences with explicit depth-bound

removing fishing for split thm in the predicate compiler

prefer recursive calls before others in the mode inference

added statistics to values command for random generation

adopting Predicate_Compile_Quickcheck

made quickcheck generic with respect to which compilation; added random compilation to quickcheck

removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command

adding a hook for experiments in the predicate compilation process

removing simple equalities in introduction rules in the predicate compiler

adopting Predicate_Compile

adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck

generalizing the compilation process of the predicate compiler

added new compilation to predicate_compiler

adding new depth-limited and new random monad for the predicate compiler

recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;

adapted to Scala 2.8.0 Beta 1;

auto update by Netbeans 6.8;

adapted to Netbeans 6.8 and Scala for Netbeans 6.8v1.1;

replaced some deprecated methods;

adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;

merged

use lattice theorems to prove set theorems

add/change some lemmas about lattices

cleaned up some proofs

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