Fri, 22 Dec 1995 11:09:28 +0100 | paulson | Improving space efficiency of inductive/datatype definitions. | file | diff | annotate |
Fri, 16 Dec 1994 17:36:50 +0100 | lcp | Defines ZF theory sections (inductive, datatype) at the start/ | file | diff | annotate |