Mon, 14 May 2012 15:54:26 +0200 blanchet repaired snag in debug function
Mon, 14 May 2012 15:54:26 +0200 blanchet graceful handling of Waldmeister endgame
Mon, 14 May 2012 15:54:26 +0200 blanchet improve parsing of Waldmeister dependencies (and kill obsolete hack)
Mon, 14 May 2012 15:54:26 +0200 blanchet tuning
Mon, 14 May 2012 15:54:26 +0200 blanchet added debugging function
Sun, 13 May 2012 16:31:01 +0200 blanchet 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
Sun, 13 May 2012 16:31:01 +0200 blanchet eta-reduce definition-like equations for THF provers; Satallax in particular seems to love that
Sun, 13 May 2012 16:31:01 +0200 blanchet 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
Sun, 13 May 2012 16:31:01 +0200 blanchet 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"
Fri, 11 May 2012 01:02:36 +0200 blanchet reintroduced example now that it's no longer broken
Fri, 11 May 2012 00:45:24 +0200 blanchet fixed "real" after they were redefined as a 'quotient_type'
Thu, 10 May 2012 22:00:24 +0200 huffman temporarily comment out broken nitpick example;
Thu, 10 May 2012 21:02:36 +0200 huffman simplify instance proofs for rat
Thu, 10 May 2012 21:18:41 +0200 huffman convert Rat.thy to use lift_definition/transfer
Thu, 10 May 2012 16:56:23 +0200 blanchet cleaner handling of bi-implication for THF output of first-order type encodings
Thu, 10 May 2012 16:56:23 +0200 blanchet distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
Thu, 10 May 2012 12:23:20 +0200 huffman temporarily comment out broken nitpick example
Thu, 10 May 2012 09:10:43 +0200 huffman convert real number theory to use lifting/transfer
Mon, 07 May 2012 15:04:17 +0200 huffman tuned ordering of lemmas
Thu, 10 May 2012 10:07:41 +0200 blanchet pass fewer facts to LEO-II and Satallax
Thu, 10 May 2012 10:07:40 +0200 blanchet tweak LEO-II setup
Thu, 10 May 2012 10:07:40 +0200 blanchet use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
Wed, 09 May 2012 11:24:38 +0200 bulwahn build Pure_64 with new settings
Wed, 09 May 2012 11:17:54 +0200 bulwahn tuned
Wed, 09 May 2012 10:39:54 +0200 bulwahn playing around with mira settings
Tue, 08 May 2012 14:35:13 +0200 bulwahn defining and proving Executable_Relation with lift_definition and transfer
Tue, 08 May 2012 14:31:03 +0200 bulwahn specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
Mon, 07 May 2012 14:50:49 +0200 blanchet prevent spurious timeouts
Mon, 07 May 2012 12:20:55 +0200 blanchet added "try0" tool to Mirabelle
Mon, 07 May 2012 12:20:55 +0200 blanchet use latest E (1.5)
Fri, 04 May 2012 17:12:37 +0200 huffman lifting package produces abs_eq_iff rules for total quotients
Fri, 04 May 2012 11:08:31 +0200 bulwahn using the new transfer method to obtain abstract properties of RBT trees
Wed, 02 May 2012 22:05:59 +0200 wenzelm back to post-release mode -- after fork point;
Wed, 23 May 2012 11:53:17 +0200 wenzelm removed obsolete RC tags;
Tue, 22 May 2012 19:02:17 +0200 wenzelm Added tag Isabelle2012 for changeset 21c42b095c84
Sun, 20 May 2012 11:34:33 +0200 wenzelm try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09); Isabelle2012
Thu, 17 May 2012 16:04:39 +0200 wenzelm Added tag Isabelle2012-RC3 for changeset ed5f56b8f90a
Thu, 17 May 2012 15:58:57 +0200 wenzelm some message;
Thu, 17 May 2012 15:23:00 +0200 wenzelm tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;
Fri, 11 May 2012 13:41:30 +0200 berghofe Fixed disambiguation of names (cf. 5759ecd5c905)
Thu, 10 May 2012 22:51:44 +0200 wenzelm merged
Thu, 10 May 2012 22:49:12 +0200 wenzelm file.encoding=UTF-8 for java.ext.dirs, to agree with java runtime invocation;
Thu, 10 May 2012 21:35:04 +0200 wenzelm prefer absolute paths, to allow launching from a different context (e.g. via file associations);
Thu, 10 May 2012 20:49:30 +0200 wenzelm tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
Wed, 09 May 2012 16:46:12 +0200 wenzelm allow spaces in target directory;
Mon, 07 May 2012 21:38:12 +0200 wenzelm Added tag Isabelle2012-RC2 for changeset 1636ff4c6243
Mon, 07 May 2012 20:35:53 +0200 wenzelm init Cygwin after unpacking;
Sun, 06 May 2012 13:58:05 +0200 wenzelm tuned proofs;
Sun, 06 May 2012 13:22:37 +0200 wenzelm more accurate ROOT.ML;
Sun, 06 May 2012 11:52:33 +0200 wenzelm prefer http://isabelle.in.tum.de/library alias, which is available at TUM only;
Sat, 05 May 2012 18:21:55 +0200 wenzelm some highlights of Isabelle2012;
Fri, 04 May 2012 17:14:42 +0200 wenzelm refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on Cygwin and appears to be redundant anyway (no extra output produced within pipe);
Fri, 04 May 2012 15:58:27 +0200 wenzelm some attempts to make critical errors fit on screen;
Thu, 03 May 2012 22:07:29 +0200 wenzelm more NEWS;
Thu, 03 May 2012 13:17:15 +0200 wenzelm backout 9579464d00f9 to avoid odd crash of polyml-5.2.1 (according to Jasmin, this change is not essential for now);
Wed, 02 May 2012 22:40:28 +0200 wenzelm Added tag Isabelle2012-RC1 for changeset ec5d54029664
Wed, 02 May 2012 22:37:50 +0200 wenzelm clarified;
Wed, 02 May 2012 21:55:13 +0200 wenzelm makedist for release;
Wed, 02 May 2012 21:23:14 +0200 wenzelm merged
Wed, 02 May 2012 21:21:51 +0200 wenzelm more contributors;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip