haftmann [Mon, 23 Aug 2010 11:09:48 +0200] rev 38668
tap_thy conversional
haftmann [Mon, 23 Aug 2010 11:09:48 +0200] rev 38667
dropped now obsolete purge_data -- happens implicitly on change of theory identity
bulwahn [Tue, 24 Aug 2010 08:22:17 +0200] rev 38666
merged
bulwahn [Mon, 23 Aug 2010 16:47:57 +0200] rev 38665
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn [Mon, 23 Aug 2010 16:47:55 +0200] rev 38664
added support for xsymbol syntax for mode annotations in code_pred command
wenzelm [Wed, 25 Aug 2010 11:13:27 +0200] rev 38663
tuned raw Sidekick output;
wenzelm [Tue, 24 Aug 2010 23:49:07 +0200] rev 38662
Text.Range.is_singleton;
wenzelm [Tue, 24 Aug 2010 21:34:38 +0200] rev 38661
Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;
wenzelm [Tue, 24 Aug 2010 21:22:01 +0200] rev 38660
tuned;
wenzelm [Tue, 24 Aug 2010 21:20:08 +0200] rev 38659
Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
tuned;
wenzelm [Tue, 24 Aug 2010 20:36:48 +0200] rev 38658
tuned root markup;
wenzelm [Mon, 23 Aug 2010 20:50:00 +0200] rev 38657
misc tuning of important special cases;
hoelzl [Mon, 23 Aug 2010 19:35:57 +0200] rev 38656
Rewrite the Probability theory.
Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
wenzelm [Mon, 23 Aug 2010 17:46:13 +0200] rev 38655
merged
blanchet [Mon, 23 Aug 2010 15:30:42 +0200] rev 38654
merged
blanchet [Mon, 23 Aug 2010 15:27:50 +0200] rev 38653
use different name for debugging purposes
blanchet [Mon, 23 Aug 2010 14:54:17 +0200] rev 38652
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes
blanchet [Mon, 23 Aug 2010 14:51:56 +0200] rev 38651
"no_atp" fact that leads to unsound Sledgehammer proofs
blanchet [Mon, 23 Aug 2010 14:21:57 +0200] rev 38650
"no_atp" fact that leads to unsound proofs in Sledgehammer
blanchet [Mon, 23 Aug 2010 12:13:58 +0200] rev 38649
"no_atp" fact that leads to unsound proofs
blanchet [Mon, 23 Aug 2010 11:56:30 +0200] rev 38648
"no_atp" a few facts that often lead to unsound proofs
blanchet [Mon, 23 Aug 2010 09:04:37 +0200] rev 38647
play with fudge factor + parse one more Vampire error
blanchet [Mon, 23 Aug 2010 00:09:25 +0200] rev 38646
fiddle a bit with the SPASS fudge number
blanchet [Sun, 22 Aug 2010 22:47:03 +0200] rev 38645
be more generous towards SPASS's -SOS mode
blanchet [Sun, 22 Aug 2010 16:56:05 +0200] rev 38644
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
haftmann [Mon, 23 Aug 2010 11:56:12 +0200] rev 38643
merged
haftmann [Mon, 23 Aug 2010 11:17:13 +0200] rev 38642
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
wenzelm [Mon, 23 Aug 2010 17:45:06 +0200] rev 38641
Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);
wenzelm [Mon, 23 Aug 2010 17:35:47 +0200] rev 38640
sporadic locking of jEdit buffer;
wenzelm [Mon, 23 Aug 2010 16:53:22 +0200] rev 38639
main session actor as independent thread, to avoid starvation via regular worker pool;
tuned;