| changeset 274 | dc87495814d5 |
| parent 250 | 9b5a069285ce |
| child 288 | b00ce6a1fe27 |
| 273:538db1a98ba3 | 274:dc87495814d5 |
|---|---|
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 The abstract types "theory" and "thm". |
6 The abstract types "theory" and "thm". |
7 Also "cterm" / "ctyp" (certified terms / typs under a signature). |
7 Also "cterm" / "ctyp" (certified terms / typs under a signature). |
8 |
8 |
9 TODO: |
|
10 NO REP_CTERM!! |
|
11 *) |
9 *) |
12 |
10 |
13 signature THM = |
11 signature THM = |
14 sig |
12 sig |
15 structure Envir : ENVIR |
13 structure Envir : ENVIR |