Tue, 22 May 2012 16:59:27 +0200 blanchet added "ext_cong_neq" lemma (not used yet); tuning
Mon, 21 May 2012 16:37:28 +0200 kuncar use quot_del instead of ML code in Rat.thy
Mon, 21 May 2012 16:36:48 +0200 kuncar quot_del attribute, it allows us to deregister quotient types
Mon, 21 May 2012 11:31:52 +0200 blanchet invite users to upgrade their SPASS (so we can get rid of old code)
Mon, 21 May 2012 11:31:52 +0200 blanchet start phasing out old SPASS
Mon, 21 May 2012 11:31:52 +0200 blanchet minor tweak in Vampire setup
Mon, 21 May 2012 11:31:52 +0200 blanchet include "ext" in all Satallax proofs
Mon, 21 May 2012 10:39:32 +0200 blanchet add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
Mon, 21 May 2012 10:39:31 +0200 blanchet tuning
Mon, 21 May 2012 10:39:31 +0200 blanchet added helper -- cf. SET616^5
Fri, 18 May 2012 17:36:20 +0200 kuncar note Quotient theorem for typedefs in setup_lifting
Fri, 18 May 2012 16:43:38 +0200 blanchet added a timeout to "try0" in Mirabelle
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip