isabelle: Changelog

huffman [Thu, 28 May 2009 17:24:18 -0700] rev 31291

fix references to dist_def

huffman [Thu, 28 May 2009 17:09:51 -0700] rev 31290

define dist for products

huffman [Thu, 28 May 2009 17:00:02 -0700] rev 31289

move dist operation to new metric_space class

huffman [Thu, 28 May 2009 14:36:21 -0700] rev 31288

remove hard tabs, fix indentation

huffman [Thu, 28 May 2009 13:52:13 -0700] rev 31287

use class field_char_0

huffman [Thu, 28 May 2009 13:43:45 -0700] rev 31286

merged

huffman [Thu, 28 May 2009 13:41:41 -0700] rev 31285

generalize dist function to class real_normed_vector

bulwahn [Thu, 28 May 2009 20:01:38 +0200] rev 31284

added remark to code

himmelma [Thu, 28 May 2009 18:59:51 +0200] rev 31283

Removed Convex_Euclidean_Space.thy from Library.

himmelma [Thu, 28 May 2009 17:03:14 +0200] rev 31282

Moved some lemmas about intervals to Topology

isabelle