isabelle: Changelog

wenzelm [Thu, 20 Mar 2014 19:24:51 +0100] rev 56229

tuned error, according to "use" in General/secure.ML;

wenzelm [Thu, 20 Mar 2014 15:38:49 +0100] rev 56228

tuned proofs;

huffman [Thu, 20 Mar 2014 15:13:55 -0700] rev 56227

generalize more theorems

huffman [Thu, 20 Mar 2014 09:21:39 -0700] rev 56226

generalize some theorems

paulson <lp15@cam.ac.uk> [Thu, 20 Mar 2014 12:43:48 +0000] rev 56225

fixing messy proofs

kleing [Thu, 20 Mar 2014 09:47:43 +0100] rev 56224

pointer to the other proof direction

huffman [Wed, 19 Mar 2014 20:50:24 -0700] rev 56223

generalize theory of operator norms to work with class real_normed_vector

wenzelm [Wed, 19 Mar 2014 23:13:45 +0100] rev 56222

tuned -- no need for slightly obscure "local" prefix;

wenzelm [Wed, 19 Mar 2014 22:26:27 +0100] rev 56221

accomodate word as part of schematic variable name;

wenzelm [Wed, 19 Mar 2014 22:10:33 +0100] rev 56220

more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);

isabelle