Wed, 19 Mar 2014 20:50:24 -0700 generalize theory of operator norms to work with class real_normed_vector
huffman [Wed, 19 Mar 2014 20:50:24 -0700] rev 56223
generalize theory of operator norms to work with class real_normed_vector
Wed, 19 Mar 2014 23:13:45 +0100 tuned -- no need for slightly obscure "local" prefix;
wenzelm [Wed, 19 Mar 2014 23:13:45 +0100] rev 56222
tuned -- no need for slightly obscure "local" prefix;
Wed, 19 Mar 2014 22:26:27 +0100 accomodate word as part of schematic variable name;
wenzelm [Wed, 19 Mar 2014 22:26:27 +0100] rev 56221
accomodate word as part of schematic variable name;
Wed, 19 Mar 2014 22:10:33 +0100 more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
wenzelm [Wed, 19 Mar 2014 22:10:33 +0100] rev 56220
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
Wed, 19 Mar 2014 21:59:31 +0100 tuned proofs;
wenzelm [Wed, 19 Mar 2014 21:59:31 +0100] rev 56219
tuned proofs;
Wed, 19 Mar 2014 18:47:22 +0100 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann [Wed, 19 Mar 2014 18:47:22 +0100] rev 56218
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 tip