Tue, 24 Aug 2010 14:41:37 +0200 hoelzl moved generic lemmas in Probability to HOL
Wed, 25 Aug 2010 11:13:58 +0200 wenzelm merged
Wed, 25 Aug 2010 09:44:54 +0200 haftmann traling newline on standard output
Wed, 25 Aug 2010 11:17:33 +0900 Cezary Kaliszyk Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Tue, 24 Aug 2010 20:09:30 +0200 blanchet merged
Tue, 24 Aug 2010 19:55:34 +0200 blanchet make Mirabelle happy
Tue, 24 Aug 2010 19:19:28 +0200 blanchet compute names lazily;
Tue, 24 Aug 2010 18:03:43 +0200 blanchet clean handling of whether a fact is chained or not;
Tue, 24 Aug 2010 16:43:52 +0200 blanchet don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
Tue, 24 Aug 2010 16:24:11 +0200 blanchet quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
Tue, 24 Aug 2010 15:29:13 +0200 blanchet revert this idea of automatically invoking "metisFT" when "metis" fails;
Tue, 24 Aug 2010 22:38:45 +0800 Christian Urban use matching of types than just equality - this is needed in nominal to cope with type variables
Tue, 24 Aug 2010 15:08:05 +0200 blanchet merge
Tue, 24 Aug 2010 15:07:54 +0200 blanchet cosmetics
Tue, 24 Aug 2010 15:06:47 +0200 blanchet use a soft time limit for E
Tue, 24 Aug 2010 14:36:29 +0200 blanchet make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
Mon, 23 Aug 2010 23:32:11 +0200 blanchet cosmetics
Mon, 23 Aug 2010 23:24:24 +0200 blanchet optimize fact filter some more
Mon, 23 Aug 2010 23:00:57 +0200 blanchet cache previous iteration's weights, and keep track of what's dirty and what's clean;
Mon, 23 Aug 2010 21:55:52 +0200 blanchet modified relevance filter
Mon, 23 Aug 2010 21:11:30 +0200 blanchet adjust fudge factors in the light of experiments
Mon, 23 Aug 2010 18:53:11 +0200 blanchet invert semantics of "relevance_convergence", to make it more intuitive
Mon, 23 Aug 2010 18:39:12 +0200 blanchet if no facts were selected on first iteration, try again with a lower threshold
Mon, 23 Aug 2010 18:25:49 +0200 blanchet weed out junk in relevance filter
Mon, 23 Aug 2010 18:04:31 +0200 blanchet no need for "eq" facts -- good old "=" is good enough for us
Mon, 23 Aug 2010 17:53:49 +0200 blanchet revert unintended change
Mon, 23 Aug 2010 17:49:18 +0200 blanchet destroy elim rules before checking for finite exhaustive facts
Mon, 23 Aug 2010 16:12:41 +0200 blanchet prevent double inclusion of the fact "True_or_False" in TPTP problems
Tue, 24 Aug 2010 10:07:14 +0200 haftmann merged
Tue, 24 Aug 2010 09:06:17 +0200 haftmann tuned
Mon, 23 Aug 2010 11:57:32 +0200 haftmann merged
Mon, 23 Aug 2010 11:57:22 +0200 haftmann dropped pre_post_conv
Mon, 23 Aug 2010 11:51:33 +0200 haftmann use conv alias
Mon, 23 Aug 2010 11:51:32 +0200 haftmann preliminary versions of static_eval_conv(_simple)
Mon, 23 Aug 2010 11:51:32 +0200 haftmann use Code_Thingol.static_eval_conv_simple
Mon, 23 Aug 2010 11:51:32 +0200 haftmann added static_eval_conv
Mon, 23 Aug 2010 11:09:49 +0200 haftmann refined and unified naming convention for dynamic code evaluation techniques
Mon, 23 Aug 2010 11:09:48 +0200 haftmann tap_thy conversional
Mon, 23 Aug 2010 11:09:48 +0200 haftmann dropped now obsolete purge_data -- happens implicitly on change of theory identity
Tue, 24 Aug 2010 08:22:17 +0200 bulwahn merged
Mon, 23 Aug 2010 16:47:57 +0200 bulwahn introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
Mon, 23 Aug 2010 16:47:55 +0200 bulwahn added support for xsymbol syntax for mode annotations in code_pred command
Wed, 25 Aug 2010 11:13:27 +0200 wenzelm tuned raw Sidekick output;
Tue, 24 Aug 2010 23:49:07 +0200 wenzelm Text.Range.is_singleton;
Tue, 24 Aug 2010 21:34:38 +0200 wenzelm Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;
Tue, 24 Aug 2010 21:22:01 +0200 wenzelm tuned;
Tue, 24 Aug 2010 21:20:08 +0200 wenzelm Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
Tue, 24 Aug 2010 20:36:48 +0200 wenzelm tuned root markup;
Mon, 23 Aug 2010 20:50:00 +0200 wenzelm misc tuning of important special cases;
Mon, 23 Aug 2010 19:35:57 +0200 hoelzl Rewrite the Probability theory.
Mon, 23 Aug 2010 17:46:13 +0200 wenzelm merged
Mon, 23 Aug 2010 15:30:42 +0200 blanchet merged
Mon, 23 Aug 2010 15:27:50 +0200 blanchet use different name for debugging purposes
Mon, 23 Aug 2010 14:54:17 +0200 blanchet perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
Mon, 23 Aug 2010 14:51:56 +0200 blanchet "no_atp" fact that leads to unsound Sledgehammer proofs
Mon, 23 Aug 2010 14:21:57 +0200 blanchet "no_atp" fact that leads to unsound proofs in Sledgehammer
Mon, 23 Aug 2010 12:13:58 +0200 blanchet "no_atp" fact that leads to unsound proofs
Mon, 23 Aug 2010 11:56:30 +0200 blanchet "no_atp" a few facts that often lead to unsound proofs
Mon, 23 Aug 2010 09:04:37 +0200 blanchet play with fudge factor + parse one more Vampire error
Mon, 23 Aug 2010 00:09:25 +0200 blanchet fiddle a bit with the SPASS fudge number
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip