equal
deleted
inserted
replaced
8 theory Datatype |
8 theory Datatype |
9 imports Inductive Univ QUniv |
9 imports Inductive Univ QUniv |
10 keywords "datatype" "codatatype" :: thy_decl |
10 keywords "datatype" "codatatype" :: thy_decl |
11 begin |
11 begin |
12 |
12 |
13 ML_file "Tools/datatype_package.ML" |
13 ML_file \<open>Tools/datatype_package.ML\<close> |
14 |
14 |
15 ML \<open> |
15 ML \<open> |
16 (*Typechecking rules for most datatypes involving univ*) |
16 (*Typechecking rules for most datatypes involving univ*) |
17 structure Data_Arg = |
17 structure Data_Arg = |
18 struct |
18 struct |