| changeset 2297 | 9ca7b249760e |
| parent 2296 | 45a69c9cc4cc |
| child 2304 | 8a98171ba1fc |
| 2296:45a69c9cc4cc | 2297:9ca7b249760e |
|---|---|
1 (* Title: nominal_dt_rawperm.ML |
1 (* Title: nominal_dt_rawfuns.ML |
2 Author: Cezary Kaliszyk |
2 Author: Cezary Kaliszyk |
3 Author: Christian Urban |
3 Author: Christian Urban |
4 |
4 |
5 Definitions of the raw bn, fv and fv_bn |
5 Definitions of the raw fv and fv_bn functions |
6 functions |
|
7 *) |
6 *) |
8 |
7 |
9 signature NOMINAL_DT_RAWFUNS = |
8 signature NOMINAL_DT_RAWFUNS = |
10 sig |
9 sig |
11 (* info of binding functions *) |
10 (* info of binding functions *) |