equal
deleted
inserted
replaced
5 |
5 |
6 header{*Datatype and CoDatatype Definitions*} |
6 header{*Datatype and CoDatatype Definitions*} |
7 |
7 |
8 theory Datatype_ZF |
8 theory Datatype_ZF |
9 imports Inductive_ZF Univ QUniv |
9 imports Inductive_ZF Univ QUniv |
|
10 keywords "datatype" "codatatype" :: thy_decl |
10 uses "Tools/datatype_package.ML" |
11 uses "Tools/datatype_package.ML" |
11 begin |
12 begin |
12 |
13 |
13 ML {* |
14 ML {* |
14 (*Typechecking rules for most datatypes involving univ*) |
15 (*Typechecking rules for most datatypes involving univ*) |