Fri, 18 May 2012 15:08:08 +0200 kuncar don't generate code in Word because it breaks the current code setup
Thu, 17 May 2012 13:36:23 +0200 blanchet robustly parse Z3 4.0's output (with outcome appearing on first rather than last line)
Thu, 17 May 2012 13:36:23 +0200 blanchet added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)
Wed, 16 May 2012 19:20:19 +0200 kuncar remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now
Wed, 16 May 2012 19:17:20 +0200 kuncar 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
Wed, 16 May 2012 19:15:45 +0200 kuncar infrastructure that makes possible to prove that a relation is reflexive
Wed, 16 May 2012 18:16:51 +0200 blanchet temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated)
Wed, 16 May 2012 18:16:51 +0200 blanchet lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
Wed, 16 May 2012 18:16:51 +0200 blanchet treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
Wed, 16 May 2012 18:16:51 +0200 blanchet get ready for automatic generation of extensionality helpers
Wed, 16 May 2012 18:16:51 +0200 blanchet minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
Wed, 16 May 2012 18:16:51 +0200 blanchet more helpful error message
Tue, 15 May 2012 12:07:16 +0200 huffman transfer rules for many more list constants
Tue, 15 May 2012 13:06:15 +0200 blanchet made SML/NJ happy
Tue, 15 May 2012 13:06:15 +0200 blanchet repair the Waldmeister endgame only for Waldmeister proofs
Tue, 15 May 2012 13:06:15 +0200 blanchet fixed Waldmeister commutativity hack
Tue, 15 May 2012 13:06:15 +0200 blanchet imported patch atp_tuning
Tue, 15 May 2012 11:50:34 +0200 huffman add transfer rules for nat_rec and funpow
Mon, 14 May 2012 17:28:07 +0200 huffman add transfer rule for constant List.lists
Mon, 14 May 2012 17:09:11 +0200 huffman add transfer rule for set_rel
Mon, 14 May 2012 15:54:26 +0200 blanchet ensure the "show" equation is not reoriented by Waldmeister
Mon, 14 May 2012 15:54:26 +0200 blanchet ensure consistent naming of Waldmeister proof steps, so that they are not cleaned away by "clean_up_atp_proof_dependencies"
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip