src/HOL/Probability/Fin_Map.thy
changeset 62102 877463945ce9
parent 62101 26c0a70f78a3
child 62343 24106dc44def
     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 17:40:59 2016 +0100
     1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 17:41:04 2016 +0100
     1.3 @@ -269,13 +269,15 @@
     1.4  begin
     1.5  
     1.6  definition [code del]:
     1.7 -  "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) = 
     1.8 +  "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) =
     1.9      (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    1.10  
    1.11 -instance 
    1.12 +instance
    1.13    by standard (rule uniformity_finmap_def)
    1.14  end
    1.15  
    1.16 +declare uniformity_Abort[where 'a="('a, 'b::metric_space) finmap", code]
    1.17 +
    1.18  instantiation finmap :: (type, metric_space) metric_space
    1.19  begin
    1.20