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