| changeset 11316 | b4e71bd751e4 |
| parent 1478 | 2b8c2a7547ab |
| child 11354 | 9b80fe19407f |
| 11315:fbca0f74bcef | 11316:b4e71bd751e4 |
|---|---|
12 consts |
12 consts |
13 data :: [i,i] => i |
13 data :: [i,i] => i |
14 |
14 |
15 datatype |
15 datatype |
16 "data(A,B)" = Con0 |
16 "data(A,B)" = Con0 |
17 | Con1 ("a: A") |
17 | Con1 ("a \\<in> A") |
18 | Con2 ("a: A", "b: B") |
18 | Con2 ("a \\<in> A", "b \\<in> B") |
19 | Con3 ("a: A", "b: B", "d: data(A,B)") |
19 | Con3 ("a \\<in> A", "b \\<in> B", "d \\<in> data(A,B)") |
20 |
20 |
21 end |
21 end |