| changeset 49834 | b27bbb021df1 |
| parent 48100 | 0122ba071e1a |
| child 51124 | 8fd094d5b7b7 |
--- a/src/HOL/Library/FinFun.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/HOL/Library/FinFun.thy Fri Oct 12 18:58:20 2012 +0200 @@ -83,7 +83,7 @@ definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}" -typedef (open) ('a,'b) finfun ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set" +typedef ('a,'b) finfun ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set" morphisms finfun_apply Abs_finfun proof - have "\<exists>f. finite {x. f x \<noteq> undefined}"