equal
deleted
inserted
replaced
5 logical operations. |
5 logical operations. |
6 *) |
6 *) |
7 |
7 |
8 signature ELEMENT = |
8 signature ELEMENT = |
9 sig |
9 sig |
|
10 type ('typ, 'term) obtain = binding * ((binding * 'typ option) list * 'term list) |
10 datatype ('typ, 'term) stmt = |
11 datatype ('typ, 'term) stmt = |
11 Shows of (Attrib.binding * ('term * 'term list) list) list | |
12 Shows of (Attrib.binding * ('term * 'term list) list) list | |
12 Obtains of (binding * ((binding * 'typ option) list * 'term list)) list |
13 Obtains of ('typ, 'term) obtain list |
13 type statement = (string, string) stmt |
14 type statement = (string, string) stmt |
14 type statement_i = (typ, term) stmt |
15 type statement_i = (typ, term) stmt |
15 datatype ('typ, 'term, 'fact) ctxt = |
16 datatype ('typ, 'term, 'fact) ctxt = |
16 Fixes of (binding * 'typ option * mixfix) list | |
17 Fixes of (binding * 'typ option * mixfix) list | |
17 Constrains of (string * 'typ) list | |
18 Constrains of (string * 'typ) list | |
59 |
60 |
60 (** language elements **) |
61 (** language elements **) |
61 |
62 |
62 (* statement *) |
63 (* statement *) |
63 |
64 |
|
65 type ('typ, 'term) obtain = binding * ((binding * 'typ option) list * 'term list); |
64 datatype ('typ, 'term) stmt = |
66 datatype ('typ, 'term) stmt = |
65 Shows of (Attrib.binding * ('term * 'term list) list) list | |
67 Shows of (Attrib.binding * ('term * 'term list) list) list | |
66 Obtains of (binding * ((binding * 'typ option) list * 'term list)) list; |
68 Obtains of ('typ, 'term) obtain list; |
67 |
69 |
68 type statement = (string, string) stmt; |
70 type statement = (string, string) stmt; |
69 type statement_i = (typ, term) stmt; |
71 type statement_i = (typ, term) stmt; |
70 |
72 |
71 |
73 |