equal
deleted
inserted
replaced
1 (* Author: Andreas Lochbihler, Uni Karlsruhe *) |
1 (* Author: Andreas Lochbihler, Uni Karlsruhe *) |
2 |
2 |
3 header {* Almost everywhere constant functions *} |
3 header {* Almost everywhere constant functions *} |
4 |
4 |
5 theory FinFun |
5 theory FinFun |
6 imports Card_Univ |
6 imports Cardinality |
7 begin |
7 begin |
8 |
8 |
9 text {* |
9 text {* |
10 This theory defines functions which are constant except for finitely |
10 This theory defines functions which are constant except for finitely |
11 many points (FinFun) and introduces a type finfin along with a |
11 many points (FinFun) and introduces a type finfin along with a |