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