changeset 515 | abcc438e7c27 |
child 935 | a94ef3eed456 |
514:ab2c867829ec | 515:abcc438e7c27 |
---|---|
1 (* Title: ZF/ex/Data.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Sample datatype definition. |
|
7 It has four contructors, of arities 0-3, and two parameters A and B. |
|
8 *) |
|
9 |
|
10 Data = Univ + |
|
11 |
|
12 consts |
|
13 data :: "[i,i] => i" |
|
14 |
|
15 datatype |
|
16 "data(A,B)" = Con0 |
|
17 | Con1 ("a: A") |
|
18 | Con2 ("a: A", "b: B") |
|
19 | Con3 ("a: A", "b: B", "d: data(A,B)") |
|
20 |
|
21 end |