merged

added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture

make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second

make Sledgehammer's "timeout" option work for "minimize"

fixed handling of "sledgehammer_params" that get a default value from Isabelle menu; and added "atp" as alias for "atps"

Spelling error: theroems -> theorems

advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.

record package: corrected sort handling in type translations to avoid crashes when default sort is changed. Test case: record 'a T = elem :: 'a defaultsort order term elem (* low-level exception *)

more precise treatment of UNC server prefix, e.g. //foo;

support named_root, which approximates UNC server prefix (for Cygwin); tuned representation: reversed elements; misc simplification and cleanup;

updated Thm.add_axiom/add_def;

adapted PUBLISH_TEST for atbroy102, which only mounts /home/isatest;

bring HOLCF/ex/Domain_Proofs.thy up to date

adapt Refute example to reflect latest soundness fix to Refute

commented out unsound "lfp"/"gfp" handling + fixed set output syntax; the "lfp"/"gfp" bug can be reproduced by looking for a counterexample to lemma "(A \<union> B)^+ = A^+ \<union> B^+" Refute incorrectly finds a countermodel for cardinality 1 (the smallest counterexample requires cardinality 2).

merged

make Nitpick output everything to tracing in debug mode; so that when an exception occurs, I can switch to the tracing window to see what was in the response window before the exception blew everything away

fix bug in Nitpick's handling of "<" (exposed by "GCD.setprod_coprime_int")

cosmetics

merge

merge

add If respectfullness and preservation to Quotient package database

more accurate pattern match

dropped dead code

update domain package examples

remove dead code

share more code between definitional and axiomatic domain packages

for axiomatic domain package, declare types and arities in domain_axioms.ML instead of domain_extender.ML

Changed the type of Quot_True, so that it is an HOL constant.

removed rather toyish tree

updated keywords

merged

user interface for abstract datatypes is an attribute, not a command

implementation of mappings by rbts

lemma is_empty_empty

constructor Mapping replaces AList

stay within Local_Defs layer;

expose foundational typedef axiom name;

Thm.add_axiom/add_def: return internal name of foundational axiom;

modernized datatype constructors;

of_sort_derivation: weaken bypasses derivation for identical sort -- accomodate proof terms by krauss/schropp, for example;

tuned;

of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;

include JEDIT_APPLE_PROPERTIES by default;

isatest: more uniform setup for Unix vs. Cygwin;

added missing case: meta universal quantifier

added imperative SAT checker; improved headers of example files; adopted IsaMakefile

Merged.

Merged resolving conflicts NEWS and locale.ML.

Proper inheritance of mixins for activated facts and locale dependencies.

Removed obsolete function.

Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.

Tuned interpretation proofs.

A rough implementation of full mixin inheritance; additional unit tests.

Clarified invariant; tuned.

More mixin tests.

Use serial to be more debug friendly.

buffered output (faster than direct output)

simplified Cache_IO interface (input is just a string and not already stored in a file)

shortened interface (do not export unused options and functions)

always unfold definitions of specific constants (including special binders)

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