| changeset 60500 | 903bb1495239 |
| parent 58881 | b9556a055632 |
| child 61384 | 9f5145281888 |
| 60499:54a3db2ed201 | 60500:903bb1495239 |
|---|---|
1 (* Author: Andreas Lochbihler, KIT *) |
1 (* Author: Andreas Lochbihler, KIT *) |
2 |
2 |
3 section {* Pretty syntax for almost everywhere constant functions *} |
3 section \<open>Pretty syntax for almost everywhere constant functions\<close> |
4 |
4 |
5 theory FinFun_Syntax |
5 theory FinFun_Syntax |
6 imports FinFun |
6 imports FinFun |
7 begin |
7 begin |
8 |
8 |