equal
deleted
inserted
replaced
1 (*Dummy theory to document dependencies *) |
1 (* Title: ZF/Datatype |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1997 University of Cambridge |
2 |
5 |
3 Datatype = "constructor" + Inductive + Univ + QUniv |
6 Dummy theory: brings in all ancestors needed for (Co)Datatype Declarations |
4 |
7 |
5 (*Datatype must be capital to avoid conflicts with ML's "datatype" *) |
8 "Datatype" must be capital to avoid conflicts with ML's "datatype" |
|
9 *) |
|
10 |
|
11 Datatype = "constructor" + Inductive + Univ + QUniv + |
|
12 |
|
13 end |
|
14 |