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;

more NEWS;

backout 9579464d00f9 to avoid odd crash of polyml-5.2.1 (according to Jasmin, this change is not essential for now);

Added tag Isabelle2012-RC1 for changeset ec5d54029664

clarified;

makedist for release;

merged

more contributors;

tuned latex sources;

more CHECKLIST;

save 90MB by removing foreign binaries -- multi-platform installations are unlikely on Windows;

some re-ordering;

some re-ordering;

tuned spelling;

resolved maxidx bug

documentation of the Lifting package on the ML level & tuned

edit NEWS items for transfer/lifting

avoid interference of markup for literal tokens, which may contain slightly odd \<^bsub> \<^esub> counted as pseudo-markup (especially relevant for HTML output, e.g. of thm power3_eq_cube);

accomodate scala-2.10.0-M3 with its extra jar; removed redundant SCALA_JARS;

more robust wrt. spaces in directory names;

updated headers;

back to "Tools" in conformance with toplevel Isabelle layout (cf. 3fabf352243e, 15f4309bb9eb);

export more symbols

merged

adding configuration to pass options to the ghc call in quickcheck[narrowing]

provide [[record_codegen]] option for skipping codegen setup for records

making sorted_list_of_set executable

removing obsolete setup for sets now that sets are executable

update references in HOLCF README

basic setup for self-extracting 7zip installer;

merged

added test case for dependency graph (cf. 2d48bf79b725)

dependency graphs: fixed direction of edges

more CHECKLIST;

more windows-friendly presentation of main text files;

split into demo and competitive version

Sledgehammer can do it

compact nat literals

some re-ordering;

some coverage of isabelle env;

updated system manual for release;

tuned;

some coverage of Isabelle/Scala tools;

some coverage of Isabelle/jEdit;

some manual updates;

some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x; removed historic note about Poly/ML vs. SML/NJ;

add isar-ref documentation for transfer package

less confusion in NEWS

rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly

renamed Semi to Seq

merged

prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;

clarified signature;

avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;

made Context_Position independent from Config;

use Nitpick as an oracle for finite problems

add extensionality to first-order provers

avoid duplicate helpers

mention tools and packages earlier;

tuned;

tuned;

tuned;

tuned;

merged

allow transfer tactic to leave extra unsolved subgoals if transfer rules are missing

documentation for the Lifting package in Isar-ref

added darwin targets;

chmod -x;

multi-platform build script and component settings;

print errors on stderr;

general exec_process -- nothing specific to Cygwin;

more direct exec with synchronous exit code;

some updates on classic README, reduce the impression that there is much to install manually;

thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)

move LEO-II closer to the top, for testing

get rid of old CASC setup and move the arithmetic part to a new theory

smaller batches, to play safe

move file to where it belongs

implement transfer tactic with more scalable forward proof methods

tuning

tweak LEO-II setup

eta-expand unapplied equalities in THF rather than using a proxy

more tweaking of TPTP/CASC setup

added a basic sanity check for quot_map

tuned comment;