equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Cartesian products *} |
6 header {* Cartesian products *} |
7 |
7 |
8 theory Product_Type |
8 theory Product_Type |
9 imports Inductive |
9 imports Typedef Inductive Fun |
10 uses |
10 uses |
11 ("Tools/split_rule.ML") |
11 ("Tools/split_rule.ML") |
12 ("Tools/inductive_set.ML") |
12 ("Tools/inductive_set.ML") |
13 ("Tools/inductive_realizer.ML") |
|
14 ("Tools/Datatype/datatype_realizer.ML") |
|
15 begin |
13 begin |
16 |
14 |
17 subsection {* @{typ bool} is a datatype *} |
15 subsection {* @{typ bool} is a datatype *} |
18 |
16 |
19 rep_datatype True False by (auto intro: bool_induct) |
17 rep_datatype True False by (auto intro: bool_induct) |
1193 val unit_all_eq1 = thm "unit_all_eq1"; |
1191 val unit_all_eq1 = thm "unit_all_eq1"; |
1194 val unit_all_eq2 = thm "unit_all_eq2"; |
1192 val unit_all_eq2 = thm "unit_all_eq2"; |
1195 val unit_eq = thm "unit_eq"; |
1193 val unit_eq = thm "unit_eq"; |
1196 *} |
1194 *} |
1197 |
1195 |
1198 |
|
1199 subsection {* Further inductive packages *} |
|
1200 |
|
1201 use "Tools/inductive_realizer.ML" |
|
1202 setup InductiveRealizer.setup |
|
1203 |
|
1204 use "Tools/inductive_set.ML" |
1196 use "Tools/inductive_set.ML" |
1205 setup Inductive_Set.setup |
1197 setup Inductive_Set.setup |
1206 |
1198 |
1207 use "Tools/Datatype/datatype_realizer.ML" |
|
1208 setup DatatypeRealizer.setup |
|
1209 |
|
1210 end |
1199 end |