src/HOL/Probability/Fin_Map.thy
changeset 50251 227477f17c26
parent 50245 dea9363887a6
child 50881 ae630bab13da
     1.1 --- a/src/HOL/Probability/Fin_Map.thy	Wed Nov 28 14:55:46 2012 +0100
     1.2 +++ b/src/HOL/Probability/Fin_Map.thy	Wed Nov 28 15:38:12 2012 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  lemma finite_domain[simp, intro]: "finite (domain P)"
     1.5    by (cases P) (auto simp: domain_def Abs_finmap_inverse)
     1.6  
     1.7 -definition proj ("_\<^isub>F" [1000] 1000) where "proj P i = snd (Rep_finmap P) i"
     1.8 +definition proj ("'((_)')\<^isub>F" [0] 1000) where "proj P i = snd (Rep_finmap P) i"
     1.9  
    1.10  declare [[coercion proj]]
    1.11