merged

update Satallax setup based on evaluation

merged

drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems

prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule

gracefully handle definition-looking premises

simplified Poly/ML setup -- 5.3.0 is now the common base-line;

discontinued support for Poly/ML 5.2.1;

less specific sample usage;

some post-release notes;

tuned names

order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy)

improved LEO-II definition handling -- still hoping for a fix directly in LEO-II

augment Satallax unsat cores with all definitions

better handling of incomplete TSTP proofs

generate THF definitions

build hybrid Isabelle component for JDK on x86-linux/x86_64-linux;

merged

eliminated old 'axioms';

discontinued obsolete method fastsimp / tactic fast_simp_tac;

eliminated obsolete fastsimp;

extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0

merged

doc updates

lower the monomorphization thresholds for less scalable provers

more explicit proof; misc tuning;

tuned proof;

prefer symbolic "contrib" -- mira should have a symlink to physical contrib_devel;

merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;

compile

don't apply "ext_cong_neq" to biimplications

added one slice with configurable simplification turned off

make higher-order goals more first-order via extensionality

added "ext_cong_neq" lemma (not used yet); tuning

use quot_del instead of ML code in Rat.thy

quot_del attribute, it allows us to deregister quotient types

invite users to upgrade their SPASS (so we can get rid of old code)

start phasing out old SPASS

minor tweak in Vampire setup

include "ext" in all Satallax proofs

add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"

tuning

added helper -- cf. SET616^5

note Quotient theorem for typedefs in setup_lifting

added a timeout to "try0" in Mirabelle

don't generate code in Word because it breaks the current code setup

robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)

added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)

remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now

generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command

infrastructure that makes possible to prove that a relation is reflexive

temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)

lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up

treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect

get ready for automatic generation of extensionality helpers

minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)

more helpful error message

transfer rules for many more list constants

made SML/NJ happy

repair the Waldmeister endgame only for Waldmeister proofs

fixed Waldmeister commutativity hack

imported patch atp_tuning

add transfer rules for nat_rec and funpow

add transfer rule for constant List.lists

add transfer rule for set_rel

ensure the "show" equation is not reoriented by Waldmeister

ensure consistent naming of Waldmeister proof steps, so that they are not cleaned away by "clean_up_atp_proof_dependencies"

repaired snag in debug function

graceful handling of Waldmeister endgame

improve parsing of Waldmeister dependencies (and kill obsolete hack)

tuning

added debugging function

LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover

eta-reduce definition-like equations for THF provers; Satallax in particular seems to love that

get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default

extend ATP data structure to avoid having to perform ((non-)capture avoiding) beta reduction -- fixes a bug in the THF translation of "is_measure.simps"

reintroduced example now that it's no longer broken

fixed "real" after they were redefined as a 'quotient_type'

temporarily comment out broken nitpick example; adapt to new definition of type rat

simplify instance proofs for rat

convert Rat.thy to use lift_definition/transfer

cleaner handling of bi-implication for THF output of first-order type encodings

distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers

temporarily comment out broken nitpick example

convert real number theory to use lifting/transfer

tuned ordering of lemmas

pass fewer facts to LEO-II and Satallax

tweak LEO-II setup

use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)

build Pure_64 with new settings

tuned

playing around with mira settings

defining and proving Executable_Relation with lift_definition and transfer

specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer

prevent spurious timeouts

added "try0" tool to Mirabelle

use latest E (1.5)

lifting package produces abs_eq_iff rules for total quotients

using the new transfer method to obtain abstract properties of RBT trees

back to post-release mode -- after fork point;

removed obsolete RC tags;

Added tag Isabelle2012 for changeset 21c42b095c84

try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

Added tag Isabelle2012-RC3 for changeset ed5f56b8f90a

some message;

tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;

Fixed disambiguation of names (cf. 5759ecd5c905)

merged

file.encoding=UTF-8 for java.ext.dirs, to agree with java runtime invocation;

prefer absolute paths, to allow launching from a different context (e.g. via file associations);

tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";

allow spaces in target directory;

Added tag Isabelle2012-RC2 for changeset 1636ff4c6243

init Cygwin after unpacking;

tuned proofs;

more accurate ROOT.ML;

prefer http://isabelle.in.tum.de/library alias, which is available at TUM only;

some highlights of Isabelle2012;

refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on Cygwin and appears to be redundant anyway (no extra output produced within pipe);

some attempts to make critical errors fit on screen;