src/HOL/Multivariate_Analysis/Operator_Norm.thy
Wed, 28 Apr 2010 15:05:45 -0700 huffman move operator norm stuff to new theory file
less more (0) tip