distinguish between the different ATP errors in the user interface; in particular, tell users to upgrade their SPASS if they try to run "spass_tptp" with an old SPASS version with no TPTP support

added "spass_tptp" prover, which requires SPASS x.y > 3.0; once users have upgraded their SPASS and we have determined that "spass_tptp" works well, we can make "spass_tptp" the one and only "spass"

use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"

merged

make profiling depend on reference Quickcheck.timing

added examples for detecting switches

adopting documentation of the predicate compiler

removing dead code; clarifying function names; removing clone

adopting examples to changes in the predicate compiler

adopting quickcheck

tuning mutabelle; adding output of mutant theoryfile for interactive evaluation

added switch detection to the predicate compiler

added further inlining of boolean constants to the predicate compiler

adding more profiling to the predicate compiler

only add relevant predicates to the list of extra modes

switched off no_topmost_reordering

replaced call to inductive package by axiomatization in the function flattening of the predicate compiler

added option for specialisation to the predicate compiler

prefer functional modes of functions in the mode analysis

added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations

merged

Only use provided SMT-certificates in HOL-Multivariate_Analysis.

Translated remaining theorems about integration from HOL light.

marked cygwin-poly as "e" test, which means further stages do not depend on it (website etc.);

replace many uses of Drule.export_without_context with Drule.zero_var_indexes

Remove garbage.

Remove garbage.

recovered isabelle java, which was broken in ebfa4bb0d50f;

fix bug in SPASS's DFG output files, where "tc_bool" wasn't declared; this bug occurs when the explicit "hAPP" or "hBOOL" functions are introduced and full types is activated

merged

added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)

merge

cosmetics

don't redo an axiom selection in the first round of Sledgehammer "minimize"!; this is needlessly slow and messes up the declared functions/predicates in SPASS DFG files

get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts

added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent

workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted

got rid of somewhat pointless "pairname" function in Sledgehammer

make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems

cosmetics

cosmetics

cosmetics

make Sledgehammer's minimizer also minimize Isar proofs

don't use readable names if proof reconstruction is needed, because it uses the structure of names

allow "_" in TPTP names in debug mode

rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does

set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format

get rid of "List.foldl" + add timestamp to SPASS

less ambitious settings for cygwin-poly;

respectfullness and preservation of map for identity quotients

respectfullness and preservation of function composition

eta-normalize the goal since the original theorem is atomized

accept x86_64 results gracefully -- NB: Mac OS does report that if booted in 64 bit mode;

refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;

merged

more appropriate representation of valid positions for abstractors

more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates

update_syntax: add new productions only once, to allow repeated local notation, for example;

tuned;

more platform information;

check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;

some updates on multi-platform support;

merged

explicit check sorts in abstract certificates; abstractor is part of dependencies

polyml-platform script is superseded by ISABELLE_PLATFORM;

less ambitious settings for cygwin-poly;

merged

more convenient equations for zip

more platform info;

added ISABELLE_PLATFORM and ISABELLE_PLATFORM64 -- NB: ML and JVM may have a different idea;

system properties determine the JVM platform, not the Isabelle one;

THIS_CYGWIN;

improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;

isatest: more robust treatment of remote files, less reliance on mounted file system;

merged

added missing \n in output

by default, don't try to start ATPs that aren't installed

fiddle with Sledgehammer option syntax

added timestamp to proof

restore order of clauses in TPTP output; there's a rather subtle invariant w.r.t. "extract_lemmas"

optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time; saves 2 sec per Sledgehammer invocation on my laptop!

output total time taken by Sledgehammer if "verbose" is set

Sledgehammer: the empty set of fact () should mean nothing, not unchanged

reorganize Sledgehammer's relevance filter slightly

tell the user that Sledgehammer kills its siblings

updated keywords;

replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix); misc tuning and simplification;

keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;

separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

allow syntax types within abbreviations;

modernized old-style type abbreviations;

modernized type abbreviations;

local type abbreviations;

merged

added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)

store nonmangled names along with mangled type names in Sledgehammer for debugging purposes

give more sensible names to "fol_type" constructors, as requested by a FIXME comment

make Sledgehammer's output more debugging friendly

made SML/NJ happy;

proper masking of dummy name_space;

salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;

proper checking of ML functors (in Poly/ML 5.2 or later); eliminated pathetic comments;

added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;

isatest: improved treatment of local files on atbroy102;

add rule deflation_ID to proof script for take + constructor rules

more robust record syntax: use Type.raw_match to ignore sort constraints as in regular abbreviations (also note that constraints only affect operations, not types);

HOL record: explicitly allow sort constraints;

misc tuning and simplification;

explicit ProofContext.check_tfree;

merged

Respectfullness and preservation of list_rel

replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo; simplified via ProofContext.check_tfree;

get_sort: suppress dummyS from input; added check_tvar, check_tfree convenience; tuned;

modernized treatment of sort constraints in specification; pass-through type variables as usual as (string * sort) internally -- recovers proper sort handling;

typecopy: observe given sort constraints more precisely;

inline old Record.read_typ/cert_typ; spelling;

spelling;

theory RBT with abstract type of red-black trees backed by implementation RBT_Impl

tuned whitespace;

merged

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;