src/HOL/Library/FinFun.thy
changeset 55565 f663fc1e653b
parent 53374 a14d2a854c02
child 58787 af9eb5e566dd
     1.1 --- a/src/HOL/Library/FinFun.thy	Tue Feb 18 23:03:49 2014 +0100
     1.2 +++ b/src/HOL/Library/FinFun.thy	Tue Feb 18 23:03:50 2014 +0100
     1.3 @@ -411,7 +411,7 @@
     1.4  qed
     1.5  
     1.6  lift_definition finfun_default :: "'a \<Rightarrow>f 'b \<Rightarrow> 'b"
     1.7 -is "finfun_default_aux" ..
     1.8 +is "finfun_default_aux" .
     1.9  
    1.10  lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
    1.11  by transfer (erule finite_finfun_default_aux)